%%%% implicate lemma.  explicit system to implicit system.

implicate/sg-wf		: esg-wf G K -> isg-wf G K -> type.
%mode implicate/sg-wf +D1 -D2.

implicate/sg-deq	: esg-deq G K1 K2 -> isg-deq G K1 K2 -> type.
%mode implicate/sg-deq +D1 -D2.

-	: implicate/sg-wf (esg-wf/sg/unit _) D
	   <- sg-wf-to-isg-wf G sg-wf/sg/unit D.

-	: implicate/sg-wf (esg-wf/sg/cn D) D''
	   <- implicate/ofkd D D'
	   <- isg-wf/sg/cn D' D''.

-	: implicate/sg-wf (esg-wf/sg/kd D) D''
	   <- implicate/kd-wf D D'
	   <- isg-wf/sg/kd D' D''.

-	: implicate/sg-wf (esg-wf/sg/sgm D1 D2 DFS) D''
	   <- implicate/sg-wf D1 D1'
	   <- ({c:cn} {d: isvar c I}
		 implicate/sg-wf (D2 c d) (isg-wf/cons (D2' c)))
	   <- isg-wf/sg/sgm D1' DFS D2' D''.

-	: implicate/sg-wf (esg-wf/sg/pi D1 D2 DFS) D''
	   <- implicate/sg-wf D1 D1'
	   <- ({c:cn} {d: isvar c I}
		 implicate/sg-wf (D2 c d) (isg-wf/cons (D2' c)))
	   <- isg-wf/sg/pi D1' DFS D2' D''.



-	: implicate/sg-deq (esg-deq/sg/unit _) D
	   <- sg-deq-to-isg-deq G sg-deq/sg/unit D.

-	: implicate/sg-deq (esg-deq/sg/cn D) D''
	   <- implicate/cn-deq D D'
	   <- isg-deq/sg/cn D' D''.

-	: implicate/sg-deq (esg-deq/sg/kd D) D''
	   <- implicate/kd-deq D D'
	   <- isg-deq/sg/kd D' D''.

-	: implicate/sg-deq (esg-deq/sg/sgm D1 D2 DFS) D''
	   <- implicate/sg-deq D1 D1'
	   <- ({c:cn} {d: isvar c I} 
		 implicate/sg-deq (D2 c d) (isg-deq/cons (D2' c)))
	   <- isg-deq/sg/sgm D1' DFS D2' D''.

-	: implicate/sg-deq (esg-deq/sg/pi D1 D2 DFS) D''
	   <- implicate/sg-deq D1 D1'
	   <- ({c:cn}  {d: isvar c I} 
		 implicate/sg-deq (D2 c d) (isg-deq/cons (D2' c)))
	   <- isg-deq/sg/pi D1' DFS D2' D''.



%worlds (ovar-block | ofkd-block)
(implicate/sg-wf _ _)
(implicate/sg-deq _ _).
%total (D1 D2)
(implicate/sg-wf D1 _)
(implicate/sg-deq D2 _).




implicate-closed/sg-wf : esg-wf cxt/nil K -> sg-wf K -> type.
%mode implicate-closed/sg-wf +X1 -X2.

-	: implicate-closed/sg-wf D D'
	   <- implicate/sg-wf D (isg-wf/nil D').

%worlds (ofkd-block) (implicate-closed/sg-wf _ _).
%total {} (implicate-closed/sg-wf _ _).



implicate-closed/sg-deq : esg-deq cxt/nil K1 K2 -> sg-deq K1 K2 -> type.
%mode implicate-closed/sg-deq +X1 -X2.

-	: implicate-closed/sg-deq D D'
	   <- implicate/sg-deq D (isg-deq/nil D').

%worlds (ofkd-block) (implicate-closed/sg-deq _ _).
%total {} (implicate-closed/sg-deq _ _).