%%%% reflexivity of kinds

sg-refl/deq : sg-wf S -> sg-deq S S -> type.
%mode sg-refl/deq +D1 -D2.

-	: sg-refl/deq sg-wf/sg/unit sg-deq/sg/unit.

-	: sg-refl/deq (sg-wf/sg/kd DK) (sg-deq/sg/kd DKS)
	   <- kd-refl/deq DK DKS.

-	: sg-refl/deq (sg-wf/sg/cn DC) (sg-deq/sg/cn (cn-deq/refl DC)).

-	: sg-refl/deq (sg-wf/sg/sgm D1 D2 DFS) (sg-deq/sg/sgm D3 D4 DFS)
	   <- sg-refl/deq D1 D3
	   <- {a:cn} {da:ofkd a _} 
	      sg-refl/deq (D2 a da) (D4 a da).

-	: sg-refl/deq (sg-wf/sg/pi D1 D2 DFS) (sg-deq/sg/pi D3 D4 DFS)
	   <- sg-refl/deq D1 D3
	   <- {a:cn} {da:ofkd a _} 
	      sg-refl/deq (D2 a da) (D4 a da).

%worlds (ofkd-block) (sg-refl/deq _ _).
%total (D1) (sg-refl/deq D1 _).



sg-refl/sub : sg-wf S -> sg-sub S S -> type.
%mode sg-refl/sub +D1 -D2.

-	: sg-refl/sub sg-wf/sg/unit sg-sub/sg/unit.

-	: sg-refl/sub (sg-wf/sg/kd DK) (sg-sub/sg/kd DKS)
	   <- kd-refl/sub DK DKS.

-	: sg-refl/sub (sg-wf/sg/cn DC) (sg-sub/sg/cn (cn-deq/refl DC)).

-	: sg-refl/sub (sg-wf/sg/sgm D1 D2 DFS) (sg-sub/sg/sgm D3 D4 D2 DFS DFS)
	   <- sg-refl/sub D1 D3
	   <- {a:cn} {da:ofkd a _} 
	      sg-refl/sub (D2 a da) (D4 a da).

-	: sg-refl/sub (sg-wf/sg/pi D1 D2 DFS) (sg-sub/sg/pi D3 D4 DFS)
	   <- sg-refl/deq D1 D3
	   <- {a:cn} {da:ofkd a _} 
	      sg-refl/deq (D2 a da) (D4 a da).

%worlds (ofkd-block) (sg-refl/sub _ _).
%total (D1) (sg-refl/sub D1 _).