%%%%%  Worlds  %%%%%

%block nbind : some {a:tp} {ea:etp}
		 block {x:atom} {d:vof x a} {ex:eterm} {xt:vtrans ex x} {ed:evof ex ea}.




%%%%%  Substitution  %%%%%

esubst-of-gen		: (evof M A -> eof N B)
			   -> (eof M A -> eof N B) -> type.
%mode esubst-of-gen +X1 -X2.

esubst-wf-gen		: (evof M A -> ewf B)
			   -> (eof M A -> ewf B) -> type.
%mode esubst-wf-gen +X1 -X2.

esubst-subtp-gen	: (evof M A -> subtp B C)
			   -> (eof M A -> subtp B C) -> type.
%mode esubst-subtp-gen +X1 -X2.

esubst-tequiv-gen	: (evof M A -> tequiv B C)
			   -> (eof M A -> tequiv B C) -> type.
%mode esubst-tequiv-gen +X1 -X2.

esubst-equiv-gen	: (evof M A -> equiv N N' B)
			   -> (eof M A -> equiv N N' B) -> type.
%mode esubst-equiv-gen +X1 -X2.


-varsam	: esubst-of-gen ([d] eof/var (D d) d) ([d] d).

-varoth	: esubst-of-gen ([d] eof/var (D2 d) D1) ([d] eof/var (D2' d) D1)
	   <- esubst-wf-gen D2 D2'.

-forall	: esubst-of-gen ([d] eof/forall (D d)) ([d] eof/forall (D' d))
	   <- esubst-wf-gen D D'.

-const	: esubst-of-gen ([d] eof/const (D2 d) D) ([d] eof/const (D2' d) D)
	   <- esubst-wf-gen D2 D2'.

-lam	: esubst-of-gen ([d] eof/lam (D2 d) (D1 d)) ([d] eof/lam (D2' d) (D1' d))
	   <- esubst-wf-gen D1 D1'
	   <- ({y} {e}
		 esubst-of-gen ([d] D2 d y e) ([d] D2' d y e)).

-app	: esubst-of-gen ([d] eof/app (D2 d) (D1 d)) ([d] eof/app (D2' d) (D1' d))
	   <- esubst-of-gen D1 D1'
	   <- esubst-of-gen D2 D2'.

-pair	: esubst-of-gen ([d] eof/pair (D3 d : {y} evof y A -> ewf (B y)) (D2 d) (D1 d)) ([d] eof/pair (D3' d) (D2' d) (D1' d))
	   <- esubst-of-gen D1 D1'
	   <- esubst-of-gen D2 D2'
	   <- ({y} {e}
		 esubst-wf-gen ([d] D3 d y e) ([d] D3' d y e)).

-pi1	: esubst-of-gen ([d] eof/pi1 (D d)) ([d] eof/pi1 (D' d))
	   <- esubst-of-gen D D'.

-pi2	: esubst-of-gen ([d] eof/pi2 (D d)) ([d] eof/pi2 (D' d))
	   <- esubst-of-gen D D'.

-sing	: esubst-of-gen ([d] eof/sing (D d)) ([d] eof/sing (D' d))
	   <- esubst-of-gen D D'.

-extpi	: esubst-of-gen ([d] eof/extpi (D2 d) (D1 d)) ([d] eof/extpi (D2' d) (D1' d))
	   <- esubst-of-gen D1 D1'
	   <- ({y} {e}
		 esubst-of-gen ([d] D2 d y e) ([d] D2' d y e)).

-extsig	: esubst-of-gen ([d] eof/extsigma (D3 d) (D2 d) (D1 d)) ([d] eof/extsigma (D3' d) (D2' d) (D1' d))
	   <- esubst-of-gen D1 D1'
	   <- esubst-of-gen D2 D2'
	   <- ({y} {e}
		 esubst-wf-gen ([d] D3 d y e) ([d] D3' d y e)).

-subsum	: esubst-of-gen ([d] eof/subsume (D2 d) (D1 d)) ([d] eof/subsume (D2' d) (D1' d))
	   <- esubst-of-gen D1 D1'
	   <- esubst-subtp-gen D2 D2'.



-t	: esubst-wf-gen ([d] ewf/t) ([d] ewf/t).

-pi	: esubst-wf-gen ([d] ewf/pi (D2 d) (D1 d)) ([d] ewf/pi (D2' d) (D1' d))
	   <- esubst-wf-gen D1 D1'
	   <- ({y} {e}
		 esubst-wf-gen ([d] D2 d y e) ([d] D2' d y e)).

-sigma	: esubst-wf-gen ([d] ewf/sigma (D2 d) (D1 d)) ([d] ewf/sigma (D2' d) (D1' d))
	   <- esubst-wf-gen D1 D1'
	   <- ({y} {e}
		 esubst-wf-gen ([d] D2 d y e) ([d] D2' d y e)).

-sing	: esubst-wf-gen ([d] ewf/sing (D d)) ([d] ewf/sing (D' d))
	   <- esubst-of-gen D D'.



-refl	: esubst-subtp-gen ([d] subtp/reflex (D d)) ([d] subtp/reflex (D' d))
	   <- esubst-tequiv-gen D D'.

-trans	: esubst-subtp-gen ([d] subtp/trans (D2 d) (D1 d)) ([d] subtp/trans (D2' d) (D1' d))
	   <- esubst-subtp-gen D1 D1'
	   <- esubst-subtp-gen D2 D2'.

-sing_t	: esubst-subtp-gen ([d] subtp/sing_t (D d)) ([d] subtp/sing_t (D' d))
	   <- esubst-of-gen D D'.

-pi	: esubst-subtp-gen ([d] subtp/pi (D3 d) (D2 d) (D1 d)) ([d] subtp/pi (D3' d) (D2' d) (D1' d))
	   <- esubst-subtp-gen D1 D1'
	   <- ({y} {e}
		 esubst-subtp-gen ([d] D2 d y e) ([d] D2' d y e))
	   <- ({y} {e}
		 esubst-wf-gen ([d] D3 d y e) ([d] D3' d y e)).

-sigma	: esubst-subtp-gen ([d] subtp/sigma (D3 d) (D2 d) (D1 d)) ([d] subtp/sigma (D3' d) (D2' d) (D1' d))
	   <- esubst-subtp-gen D1 D1'
	   <- ({y} {e}
		 esubst-subtp-gen ([d] D2 d y e) ([d] D2' d y e))
	   <- ({y} {e}
		 esubst-wf-gen ([d] D3 d y e) ([d] D3' d y e)).



-refl	: esubst-tequiv-gen ([d] tequiv/reflex (D d)) ([d] tequiv/reflex (D' d))
	   <- esubst-wf-gen D D'.

-symm	: esubst-tequiv-gen ([d] tequiv/symm (D d)) ([d] tequiv/symm (D' d))
	   <- esubst-tequiv-gen D D'.

-trans	: esubst-tequiv-gen ([d] tequiv/trans (D2 d) (D1 d)) ([d] tequiv/trans (D2' d) (D1' d))
	   <- esubst-tequiv-gen D1 D1'
	   <- esubst-tequiv-gen D2 D2'.

-pi	: esubst-tequiv-gen ([d] tequiv/pi (D2 d) (D1 d)) ([d] tequiv/pi (D2' d) (D1' d))
	   <- esubst-tequiv-gen D1 D1'
	   <- ({y} {e}
		 esubst-tequiv-gen ([d] D2 d y e) ([d] D2' d y e)).

-sigma	: esubst-tequiv-gen ([d] tequiv/sigma (D2 d) (D1 d)) ([d] tequiv/sigma (D2' d) (D1' d))
	   <- esubst-tequiv-gen D1 D1'
	   <- ({y} {e}
		 esubst-tequiv-gen ([d] D2 d y e) ([d] D2' d y e)).

-sing	: esubst-tequiv-gen ([d] tequiv/sing (D d)) ([d] tequiv/sing (D' d))
	   <- esubst-equiv-gen D D'.



-refl	: esubst-equiv-gen ([d] equiv/reflex (D d)) ([d] equiv/reflex (D' d))
	   <- esubst-of-gen D D'.

-symm	: esubst-equiv-gen ([d] equiv/symm (D d)) ([d] equiv/symm (D' d))
	   <- esubst-equiv-gen D D'.

-trans	: esubst-equiv-gen ([d] equiv/trans (D2 d) (D1 d)) ([d] equiv/trans (D2' d) (D1' d))
	   <- esubst-equiv-gen D1 D1'
	   <- esubst-equiv-gen D2 D2'.


-forall	: esubst-equiv-gen ([d] equiv/forall (D d)) ([d] equiv/forall (D' d))
	   <- esubst-tequiv-gen D D'.

-lam	: esubst-equiv-gen ([d] equiv/lam (D2 d) (D1 d)) ([d] equiv/lam (D2' d) (D1' d))
	   <- esubst-tequiv-gen D1 D1'
	   <- ({y} {e}
		 esubst-equiv-gen ([d] D2 d y e) ([d] D2' d y e)).

-app	: esubst-equiv-gen ([d] equiv/app (D2 d) (D1 d)) ([d] equiv/app (D2' d) (D1' d))
	   <- esubst-equiv-gen D1 D1'
	   <- esubst-equiv-gen D2 D2'.

-pair	: esubst-equiv-gen ([d] equiv/pair (D3 d : {y} evof y A -> ewf (B y)) (D2 d) (D1 d)) ([d] equiv/pair (D3' d) (D2' d) (D1' d))
	   <- esubst-equiv-gen D1 D1'
	   <- esubst-equiv-gen D2 D2'
	   <- ({y} {e}
		 esubst-wf-gen ([d] D3 d y e) ([d] D3' d y e)).

-pi1	: esubst-equiv-gen ([d] equiv/pi1 (D d)) ([d] equiv/pi1 (D' d))
	   <- esubst-equiv-gen D D'.

-pi2	: esubst-equiv-gen ([d] equiv/pi2 (D d)) ([d] equiv/pi2 (D' d))
	   <- esubst-equiv-gen D D'.

-sing	: esubst-equiv-gen ([d] equiv/sing (D d)) ([d] equiv/sing (D' d))
	   <- esubst-equiv-gen D D'.

-singel	: esubst-equiv-gen ([d] equiv/singelim (D d)) ([d] equiv/singelim (D' d))
	   <- esubst-of-gen D D'.

-extpi	: esubst-equiv-gen ([d] equiv/extpi (D3 d) (D2 d) (D1 d)) ([d] equiv/extpi (D3' d) (D2' d) (D1' d))
	   <- esubst-of-gen D1 D1'
	   <- esubst-of-gen D2 D2'
	   <- ({y} {e}
		 esubst-equiv-gen ([d] D3 d y e) ([d] D3' d y e)).

-extpiw	: esubst-equiv-gen ([d] equiv/extpiw (D2 d) (D1 d)) ([d] equiv/extpiw (D2' d) (D1' d))
	   <- esubst-equiv-gen D1 D1'
	   <- ({y} {e}
		 esubst-equiv-gen ([d] D2 d y e) ([d] D2' d y e)).

-extsig	: esubst-equiv-gen ([d] equiv/extsigma (D3 d) (D2 d) (D1 d)) ([d] equiv/extsigma (D3' d) (D2' d) (D1' d))
	   <- esubst-equiv-gen D1 D1'
	   <- esubst-equiv-gen D2 D2'
	   <- ({y} {e}
		 esubst-wf-gen ([d] D3 d y e) ([d] D3' d y e)).

-subsum	: esubst-equiv-gen ([d] equiv/subsume (D2 d) (D1 d)) ([d] equiv/subsume (D2' d) (D1' d))
	   <- esubst-equiv-gen D1 D1'
	   <- esubst-subtp-gen D2 D2'.

-beta	: esubst-equiv-gen ([d] equiv/beta (D2 d) (D1 d)) ([d] equiv/beta (D2' d) (D1' d))
	   <- ({y} {e}
		 esubst-of-gen ([d] D1 d y e) ([d] D1' d y e))
	   <- esubst-of-gen D2 D2'.

-beta1	: esubst-equiv-gen ([d] equiv/beta1 (D2 d) (D1 d)) ([d] equiv/beta1 (D2' d) (D1' d))
	   <- esubst-of-gen D1 D1'
	   <- esubst-of-gen D2 D2'.

-beta2	: esubst-equiv-gen ([d] equiv/beta2 (D2 d) (D1 d)) ([d] equiv/beta2 (D2' d) (D1' d))
	   <- esubst-of-gen D1 D1'
	   <- esubst-of-gen D2 D2'.

%worlds (evar | eofblock | ebind) (esubst-of-gen _ _) (esubst-wf-gen _ _) (esubst-subtp-gen _ _) (esubst-tequiv-gen _ _) (esubst-equiv-gen _ _).
%total (D1 D2 D3 D4 D5) (esubst-of-gen D1 _) (esubst-wf-gen D2 _) (esubst-subtp-gen D3 _) (esubst-tequiv-gen D4 _) (esubst-equiv-gen D5 _).



esubst : ({x} evof x A -> eof (M x) (B x))
	  -> eof N A
	  -> eof (M N) (B N) -> type.
%mode esubst +X1 +X2 -X3.

-	: esubst D1 D2 (D1' D2)
	   <- esubst-of-gen (D1 _) D1'.

%worlds (evar | eofblock | ebind) (esubst _ _ _).
%total {} (esubst _ _ _).



esubst-subtp : ({x} evof x A -> subtp (B x) (EC x))
		-> eof N A
		-> subtp (B N) (EC N) -> type.
%mode esubst-subtp +X1 +X2 -X3.

-	: esubst-subtp D1 D2 (D1' D2)
	   <- esubst-subtp-gen (D1 _) D1'.

%worlds (evar | eofblock | ebind) (esubst-subtp _ _ _).
%total {} (esubst-subtp _ _ _).



esubst-wf : ({x} evof x A -> ewf (B x))
	     -> eof N A
	     -> ewf (B N) -> type.
%mode esubst-wf +X1 +X2 -X3.

-	: esubst-wf D1 D2 (D1' D2)
	   <- esubst-wf-gen (D1 _) D1'.

%worlds (evar | eofblock | ebind) (esubst-wf _ _ _).
%total {} (esubst-wf _ _ _).



esubst-equiv : ({x} evof x A -> equiv (M x) (M' x) (B x))
		-> eof N A
		-> equiv (M N) (M' N) (B N) -> type.
%mode esubst-equiv +X1 +X2 -X3.

-	: esubst-equiv D1 D2 (D1' D2)
	   <- esubst-equiv-gen (D1 _) D1'.

%worlds (evar | eofblock | ebind) (esubst-equiv _ _ _).
%total {} (esubst-equiv _ _ _).



esubst-tequiv : ({x} evof x A -> tequiv (B x) (B' x))
		 -> eof N A
		 -> tequiv (B N) (B' N) -> type.
%mode esubst-tequiv +X1 +X2 -X3.

-	: esubst-tequiv D1 D2 (D1' D2)
	   <- esubst-tequiv-gen (D1 _) D1'.

%worlds (evar | eofblock | ebind) (esubst-tequiv _ _ _).
%total {} (esubst-tequiv _ _ _).