nat : type.

z : nat.
s : nat -> nat.



tm : type.

tmnat	: nat -> tm.
pair	: tm -> tm -> tm.
fst	: tm -> tm.
snd	: tm -> tm.



eval	: tm -> tm -> type.

eval/nat	: eval (tmnat N) (tmnat N).
eval/pair	: eval E1 E1'
		   -> eval E2 E2'
		   -> eval (pair E1 E2) (pair E1' E2').
eval/fst	: eval E (pair E1 E2)
		   -> eval (fst E) E1.
eval/snd	: eval E (pair E1 E2)
		   -> eval (snd E) E2.



tp : type.

tp/nat		: tp.
tp/cross	: tp -> tp -> tp.



of	: tm -> tp -> type.

of/nat	: of (tmnat N) tp/nat.
of/pair	: of E1 T1
	   -> of E2 T2
	   -> of (pair E1 E2) (tp/cross T1 T2).
of/fst	: of E (tp/cross T1 T2)
	   -> of (fst E) T1.
of/snd	: of E (tp/cross T1 T2)
	   -> of (snd E) T2.



preserve	: eval E E'
		   -> of E T
		   -> of E' T
		   -> type.
%mode preserve +D1 +D2 -D3.

- : preserve eval/nat of/nat of/nat.

- : preserve (eval/pair R1 R2) (of/pair D1 D2) 
     (of/pair D1' D2')
     <- preserve R1 D1 D1'
     <- preserve R2 D2 D2'.

- : preserve (eval/fst R1) (of/fst D1) DL
     <- preserve R1 D1 (of/pair DL _).

- : preserve (eval/snd R1) (of/snd D1) DR
     <- preserve R1 D1 (of/pair _ DR).

%worlds () (preserve _ _ _).
%total (D1) (preserve D1 _ _).



proj	: (tm -> tm) -> type.

proj/id	: proj ([t] t).
proj/fst	: proj F -> proj ([t] fst (F t)).
proj/snd	: proj F -> proj ([t] snd (F t)).



proj-tp	: proj F -> tp -> tp -> type.

proj-tp/id	: proj-tp proj/id T T.
proj-tp/fst	: proj-tp P T (tp/cross T1 T2) -> proj-tp (proj/fst P) T T1.
proj-tp/snd	: proj-tp P T (tp/cross T1 T2) -> proj-tp (proj/snd P) T T2.



exp	: type.
explist	: type.

explist/nil	: explist.
explist/cons	: exp -> explist -> explist.



exp/nat		: nat -> exp.

exp/group	: explist -> exp.

exp/select	: exp -> nat -> exp.



elab-select	: nat -> proj F -> type.
elab-select/z	: elab-select z (proj/fst proj/id).
elab-select/s	: elab-select N P
		   -> elab-select (s N) (proj/snd P).



elab-exp	: exp -> tm -> tp -> type.
elab-explist	: explist -> tm -> tp -> type.

elab-exp/nat	: elab-exp (exp/nat N) (tmnat N) tp/nat.
elab-exp/group	: elab-explist EL TM TP
		   -> elab-exp (exp/group EL) TM TP.
elab-exp/select	: elab-exp E TM TP
		   -> elab-select N (P : proj F)
		   -> proj-tp P TP TP'
		   -> elab-exp (exp/select E N) (F TM) TP'.



elab-explist/nil	: elab-explist explist/nil (tmnat z) tp/nat.
elab-explist/cons	: elab-exp E TM1 TP1
			   -> elab-explist EL TM2 TP2
			   -> elab-explist (explist/cons E EL) 
			      (pair TM1 TM2) (tp/cross TP1 TP2).



proj-tp-safe	: {P: proj F}
		   proj-tp P T1 T2
		   -> of E T1
		   -> of (F E) T2
		   -> type.
%mode proj-tp-safe +D1 +D2 +D3 -D4.

-	: proj-tp-safe _ proj-tp/id D1 D1.

-	: proj-tp-safe _ (proj-tp/fst P) D1 (of/fst D2)
	   <- proj-tp-safe _ P D1 D2.

-	: proj-tp-safe _ (proj-tp/snd P) D1 (of/snd D2)
	   <- proj-tp-safe _ P D1 D2.

%worlds () (proj-tp-safe _ _ _ _).
%total (D1) (proj-tp-safe D1 _ _ _).



elab-exp-safe	: elab-exp E TM TP
		   -> of TM TP
		   -> type.
%mode elab-exp-safe +D1 -D2.

elab-explist-safe	: elab-explist EL TM TP
			   -> of TM TP
			   -> type.
%mode elab-explist-safe +D1 -D2.

-	: elab-exp-safe elab-exp/nat of/nat.

-	: elab-exp-safe (elab-exp/group EL) D1
	   <- elab-explist-safe EL D1.

-	: elab-exp-safe (elab-exp/select E _ P) D2
	   <- elab-exp-safe E D1
	   <- proj-tp-safe _ P D1 D2.

-	: elab-explist-safe elab-explist/nil of/nat.

-	: elab-explist-safe (elab-explist/cons E EL) (of/pair D1 D2)
	   <- elab-exp-safe E D1
	   <- elab-explist-safe EL D2.

%worlds () (elab-exp-safe _ _) (elab-explist-safe _ _).
%total (D1 D2) (elab-exp-safe D1 _) (elab-explist-safe D2 _).