tp : type.

b : tp.
arrow : tp -> tp -> tp.
prod : tp -> tp -> tp.

rtm : type.
mtm : type.

app : rtm -> mtm -> rtm.
c : rtm.
fst : rtm -> rtm.
snd : rtm -> rtm.

asm : rtm -> mtm.
lam : (rtm -> mtm) -> mtm.
pair : mtm -> mtm -> mtm.

%block rtm_block : block {x : rtm}.
%worlds (rtm_block) (tp) (rtm) (mtm).

atom : rtm -> tp -> type.
%mode atom +X1 -X2.

canon : mtm -> tp -> type.
%mode canon +X1 +X2.

% atomic 

atom_c : atom c b.

atom_app : atom (app R1 M2) A
            <- atom R1 (arrow A2 A)
            <- canon M2 A2.

atom_fst : atom (fst R) A1
            <- atom R (prod A1 A2).

atom_snd : atom (snd R) A2
            <- atom R (prod A1 A2).

%% canonical 

canon_asm : canon (asm R) b
             <- atom R b.

canon_lam : canon (lam M) (arrow A2 A)
             <- {x : rtm} (atom x A2) ->  canon (M x) A.

canon_pair : canon (pair M1 M2) (prod A1 A2)
              <- canon M1 A1
              <- canon M2 A2.

%block atom_block : some {A:tp}
                     block {x:rtm} {dx : atom x A}. 
%worlds (atom_block) (atom _ _) (canon _ _).
%terminates (R M) (atom R _) (canon M _).

hsubst_m : mtm -> tp -> (rtm -> mtm) -> mtm -> type.
%mode hsubst_m +X1 +X2 +X3 -X4.

hsubst_r : mtm -> tp -> (rtm -> rtm) -> rtm -> type.
%mode hsubst_r +X1 +X2 +X3 -X4.

hsubst_rr : mtm -> tp -> (rtm -> rtm) -> mtm -> tp -> type.
%mode hsubst_rr +X1 +X2 +X3 -X4 -X5.

%% Ms

hsubst_m_r : hsubst_m M0 A0 ([x] asm (R x)) (asm R')
              <- hsubst_r M0 A0 R R'.

hsubst_m_rr : hsubst_m M0 A0 ([x] asm (R x)) M'
               <- hsubst_rr M0 A0 R M' _.

hsubst_m_lam : hsubst_m M0 A0 ([x] (lam ([y] M x y))) (lam M')
                <- ({y:rtm} 
                      hsubst_m M0 A0 ([x] M x y) (M' y)).

hsubst_m_pair : hsubst_m M0 A0 ([x] (pair (M1 x) (M2 x))) (pair M1' M2')
                 <- hsubst_m M0 A0 M1 M1'
                 <- hsubst_m M0 A0 M2 M2'.

%% R not head

hsubst_r_closed : hsubst_r M0 A0 ([x] E) E.

hsubst_r_app : hsubst_r M0 A0 ([x] (app (R x) (M x))) (app R' M')
                <- hsubst_r M0 A0 R R'
                <- hsubst_m M0 A0 M M'.

hsubst_r_fst : hsubst_r M0 A0 ([x] (fst (R x))) (fst R')
                <- hsubst_r M0 A0 R R'.

hsubst_r_snd : hsubst_r M0 A0 ([x] (snd (R x))) (snd R')
                <- hsubst_r M0 A0 R R'.

%% r head

hsubst_rr_var : hsubst_rr M0 A0 ([x] x) M0 A0.

hsubst_rr_app : hsubst_rr M0 A0 ([x] app (R1 x) (M2 x)) M'' A
                 <- hsubst_rr M0 A0 R1 (lam M') (arrow A2 A)
                 <- hsubst_m M0 A0 M2 M2'
                 <- hsubst_m M2' A2 M' M''.

hsubst_rr_fst : hsubst_rr M0 A0 ([x] (fst (R x))) M1' A1'
                 <- hsubst_rr M0 A0 R (pair M1' M2') (prod A1' A2').

hsubst_rr_snd : hsubst_rr M0 A0 ([x] (snd (R x))) M2' A2'
                 <- hsubst_rr M0 A0 R (pair M1' M2') (prod A1' A2').

%worlds (rtm_block) (hsubst_m _ _ _ _) (hsubst_r _ _ _ _) (hsubst_rr _ _ _ _ _).
%reduces A' <= A0 (hsubst_rr _ A0 _ _ A').
%terminates {(A0 A0' A0'') (M R R')} (hsubst_m _ A0 M _) (hsubst_r _ A0' R _) (hsubst_rr _ A0'' R' _ _).

expand : tp -> rtm -> mtm -> type.
%mode expand +X1 +X2 -X3.

expand_b : expand b R (asm R).

expand_arrow : expand (arrow A2 A) R (lam M)
                <- ({x : rtm} expand A2 x (M2 x))
                <- ({x : rtm} expand A (app R (M2 x)) (M x)).

expand_prod : expand (prod A1 A2) R (pair M1 M2)
               <- expand A1 (fst R) M1
               <- expand A2 (snd R) M2.

%worlds (rtm_block) (expand _ _ _).
%total A (expand A _ _).

hsubst_rr_size : {A2} {A'} hsubst_rr M2 A2 R M' A'
                    -> type.
%mode hsubst_rr_size +X1 +X2 +X3.

- : hsubst_rr_size 
     A2 A2 hsubst_rr_var.

- : hsubst_rr_size
     A2 A4 (hsubst_rr_app _ _ Drr)
     <- hsubst_rr_size A2 (arrow A3 A4) Drr.

- : hsubst_rr_size
     A2 Al (hsubst_rr_fst Drr)
     <- hsubst_rr_size A2 (prod Al Ar) Drr.

- : hsubst_rr_size
     A2 Ar (hsubst_rr_snd Drr)
     <- hsubst_rr_size A2 (prod Al Ar) Drr.

%worlds (rtm_block) (hsubst_rr_size _ _ _).
%total D (hsubst_rr_size _ _ D).
%reduces A' <= A2 (hsubst_rr_size A2 A' _).
 
hsubst_r_exists_sum : mtm -> tp -> (rtm -> rtm) -> tp -> type.
hsubst_r_exists_sum_r : hsubst_r_exists_sum M2 A2 R A
                         <- hsubst_r M2 A2 R R'
                         <- atom R' A.
hsubst_r_exists_sum_rr : hsubst_r_exists_sum M2 A2 R A'
                          <- hsubst_rr M2 A2 R M' A'
                          <- canon M' A'.

hsubst_m_exists_asm :  hsubst_r_exists_sum M2 A2 R b
                       -> hsubst_m M2 A2 ([x] (asm (R x))) M'
                       -> canon M' b
                       -> type.
%mode hsubst_m_exists_asm +X1 -X2 -X3.

- : hsubst_m_exists_asm 
     (hsubst_r_exists_sum_r DaR' DsR)
     (hsubst_m_r DsR)
     (canon_asm DaR').

- : hsubst_m_exists_asm 
     (hsubst_r_exists_sum_rr DcM' DsR)
     (hsubst_m_rr DsR)
     DcM'.

%worlds (atom_block) (hsubst_m_exists_asm _ _ _).
%total {} (hsubst_m_exists_asm _ _ _).


hsubst_r_exists_fst : hsubst_r_exists_sum M2 A2 R (prod Al Ar)
                       -> hsubst_r_exists_sum M2 A2 ([x] (fst (R x))) Al
                       -> type.
%mode hsubst_r_exists_fst +X1 -X2.

- : hsubst_r_exists_fst 
     (hsubst_r_exists_sum_r DaR' DsR)
     (hsubst_r_exists_sum_r (atom_fst DaR') (hsubst_r_fst DsR)).

- : hsubst_r_exists_fst 
     (hsubst_r_exists_sum_rr (canon_pair _ DcMl') DsR)
     (hsubst_r_exists_sum_rr DcMl' (hsubst_rr_fst DsR)).

%worlds (atom_block) (hsubst_r_exists_fst _ _).
%total {} (hsubst_r_exists_fst _ _).


hsubst_r_exists_snd : hsubst_r_exists_sum M2 A2 R (prod Al Ar)
                       -> hsubst_r_exists_sum M2 A2 ([x] (snd (R x))) Ar
                       -> type.
%mode hsubst_r_exists_snd +X1 -X2.

- : hsubst_r_exists_snd 
     (hsubst_r_exists_sum_r DaR' DsR)
     (hsubst_r_exists_sum_r (atom_snd DaR') (hsubst_r_snd DsR)).

- : hsubst_r_exists_snd 
     (hsubst_r_exists_sum_rr (canon_pair DcMr' _) DsR)
     (hsubst_r_exists_sum_rr DcMr' (hsubst_rr_snd DsR)).

%worlds (atom_block) (hsubst_r_exists_snd _ _).
%total {} (hsubst_r_exists_snd _ _).

hsubst_m_exists : {A2}
                   ({y : rtm} {dy : atom y A2} canon (M y) A)
                   -> canon M2 A2
                   -> hsubst_m M2 A2 M M'
                   -> canon M' A
                   -> type.
%mode hsubst_m_exists +X0 +X1 +X2 -X3 -X4.

hsubst_r_exists : {A2}
                   ({y : rtm} {dx : atom y A2} atom (R y) A)
                   -> canon M2 A2
                   -> hsubst_r_exists_sum M2 A2 R A
                   -> type.
%mode hsubst_r_exists +X0 +X1 +X2 -X3.

hsubst_m_exists_app : {A2}
                       %% this next argument is makes the termination argument work
                       ({y : rtm} {dx : atom y A2} atom (R1 y) (arrow A3 A4)) 
                       -> hsubst_r_exists_sum M2 A2 R1 (arrow A3 A4)
                       -> hsubst_m M2 A2 M3 M3'
                       -> canon M3' A3
                       -> hsubst_r_exists_sum M2 A2 ([x] (app (R1 x) (M3 x))) A4
                       -> type.
%mode hsubst_m_exists_app +X-1 +X0 +X1 +X2 +X3 -X4.

%% canonical terms

- : hsubst_m_exists 
     A2
     ([x] [dx] canon_asm (DaR x dx))
     DcM2
     DsR
     DcM'
     <- hsubst_r_exists A2 DaR DcM2 Dsum
     <- hsubst_m_exists_asm Dsum DsR DcM'.

- : hsubst_m_exists 
     A2
     ([x] [dx] (canon_lam ([y] [dy] DcM x dx y dy)) : canon (lam (M x)) (arrow Af At))
     (DcM2 : canon M2 A2)
     (hsubst_m_lam DsM)
     (canon_lam DcM')
     <- ({y} 
           {dy : atom y Af}
           hsubst_m_exists A2 ([x] [dx] (DcM x dx y dy)) DcM2 (DsM y) (DcM' y dy)).

- : hsubst_m_exists
     A2
     ([x] [dx] (canon_pair (DcMr x dx) (DcMl x dx)))
     DcM2
     (hsubst_m_pair DsMr DsMl)
     (canon_pair DcMr' DcMl')
     <- hsubst_m_exists A2 DcMl DcM2 DsMl DcMl'
     <- hsubst_m_exists A2 DcMr DcM2 DsMr DcMr'.

%% atomic terms

- : hsubst_r_exists 
     A2
     ([x] [dx] D)
     _
     (hsubst_r_exists_sum_r D hsubst_r_closed).

- : hsubst_r_exists
     A2
     ([x] [dx] dx)
     DcM2
     (hsubst_r_exists_sum_rr DcM2 hsubst_rr_var).

- : hsubst_r_exists
     A2
     ([x] [dx] (atom_app (DcM x dx) (DaR x dx)))
     DcM2
     DsumApp
     <- hsubst_m_exists A2 DcM DcM2 DsM' DcM'
     <- hsubst_r_exists A2 DaR DcM2 DsumR'
     <- hsubst_m_exists_app A2 DaR DsumR' DsM' DcM' DsumApp.

- : hsubst_r_exists
     A2
     ([x] [dx] (atom_fst (DcR x dx)))
     DcM2
     DsumFst
     <- hsubst_r_exists A2 DcR DcM2 DsumR
     <- hsubst_r_exists_fst DsumR DsumFst.

- : hsubst_r_exists
     A2
     ([x] [dx] (atom_snd (DcR x dx)))
     DcM2
     DsumSnd
     <- hsubst_r_exists A2 DcR DcM2 DsumR
     <- hsubst_r_exists_snd DsumR DsumSnd.

%% app factoring lemma

- : hsubst_m_exists_app 
     A2 
     _
     (hsubst_r_exists_sum_r DaR1 DsR1)
     DsM3
     DcM3
     (hsubst_r_exists_sum_r (atom_app DcM3 DaR1) (hsubst_r_app DsM3 DsR1)).

- : hsubst_m_exists_app 
     A2
     _
     (hsubst_r_exists_sum_rr (canon_lam DcM4') DsR1)
     DsM3
     DcM3
     (hsubst_r_exists_sum_rr DcM4'' (hsubst_rr_app DsM4' DsM3 DsR1))
     <- hsubst_rr_size A2 (arrow A3 A4) DsR1
     <- hsubst_m_exists A3 DcM4' DcM3 DsM4' DcM4''.

%worlds (atom_block) 
(hsubst_m_exists_app _ _ _ _ _ _)
(hsubst_r_exists _ _ _ _)
(hsubst_m_exists _ _ _ _ _).

%total {(A2 A2' A2'') (D  D' D'')}
(hsubst_m_exists A2' D' _ _ _)
(hsubst_m_exists_app A2'' D'' _ _ _ _)
(hsubst_r_exists A2 D _ _).

id/mtm : mtm -> mtm -> type.
id/mtm_refl : id/mtm M M.

id/rtm : rtm -> rtm -> type.
id/rtm_refl : id/rtm R R.

id/tp : tp -> tp -> type.
id/tp_refl : id/tp A A.

id/rtm_sym : id/rtm R R'
	      -> id/rtm R' R
	      -> type.
%mode id/rtm_sym +X1 -X2.

- : id/rtm_sym id/rtm_refl id/rtm_refl.

%worlds (rtm_block) (id/rtm_sym _ _).
%total {} (id/rtm_sym _ _).

id/tp_arrow_inv : id/tp (arrow A1 A2) (arrow A1' A2')
		   -> id/tp A1 A1'
		   -> id/tp A2 A2'
		   -> type.
%mode id/tp_arrow_inv +X1 -X2 -X3.

- : id/tp_arrow_inv _ id/tp_refl id/tp_refl.

%worlds (rtm_block) (id/tp_arrow_inv _ _ _).
%total {} (id/tp_arrow_inv _ _ _).

id/tp_prod_inv : id/tp (prod A1 A2) (prod A1' A2')
		   -> id/tp A1 A1'
		   -> id/tp A2 A2'
		   -> type.
%mode id/tp_prod_inv +X1 -X2 -X3.

- : id/tp_prod_inv _ id/tp_refl id/tp_refl.

%worlds (rtm_block) (id/tp_prod_inv _ _ _).
%total {} (id/tp_prod_inv _ _ _).

id/rtm_app_cong : id/rtm R R'
		   -> id/mtm M M'
		   -> id/rtm (app R M) (app R' M')
		   -> type.
%mode id/rtm_app_cong +X1 +X2 -X3.

- : id/rtm_app_cong _ _ id/rtm_refl.

%worlds (rtm_block) (id/rtm_app_cong _ _ _).
%total {} (id/rtm_app_cong _ _ _).

id/rtm_fst_cong : id/rtm R R'
		   -> id/rtm (fst R) (fst R')
		   -> type.
%mode id/rtm_fst_cong +X1  -X3.

- : id/rtm_fst_cong _ id/rtm_refl.

%worlds (rtm_block) (id/rtm_fst_cong _ _).
%total {} (id/rtm_fst_cong _ _).

id/rtm_snd_cong : id/rtm R R'
		   -> id/rtm (snd R) (snd R')
		   -> type.
%mode id/rtm_snd_cong +X1  -X3.

- : id/rtm_snd_cong _ id/rtm_refl.

%worlds (rtm_block) (id/rtm_snd_cong _ _).
%total {} (id/rtm_snd_cong _ _).

id/mtm_lam_cong :  ({x:rtm} id/mtm (M x) (M' x))
		   -> id/mtm (lam M) (lam M')
		   -> type.
%mode id/mtm_lam_cong +X1 -X3.

- : id/mtm_lam_cong _ id/mtm_refl.

%worlds (rtm_block) (id/mtm_lam_cong _ _).
%total {} (id/mtm_lam_cong _ _).

id/mtm_lam_inv :  id/mtm (lam M) (lam M')
		  -> ({x:rtm} id/mtm (M x) (M' x))
		  -> type.
%mode id/mtm_lam_inv +X1 -X3.

- : id/mtm_lam_inv _ ([_] id/mtm_refl).

%worlds (rtm_block) (id/mtm_lam_inv _ _).
%total {} (id/mtm_lam_inv _ _).

id/mtm_pair_cong : id/mtm M1 M1'
		   -> id/mtm M2 M2'
		   -> id/mtm (pair M1 M2) (pair M1' M2')
		   -> type.
%mode id/mtm_pair_cong +X1 +X2 -X3.

- : id/mtm_pair_cong _ _ id/mtm_refl.

%worlds (rtm_block) (id/mtm_pair_cong _ _ _).
%total {} (id/mtm_pair_cong _ _ _).

id/mtm_pair_inv : id/mtm (pair M1 M2) (pair M1' M2')
		   -> id/mtm M1 M1'
		   -> id/mtm M2 M2'
		   -> type.
%mode id/mtm_pair_inv +X1 -X2 -X3.

- : id/mtm_pair_inv _ id/mtm_refl id/mtm_refl.

%worlds (rtm_block) (id/mtm_pair_inv _ _ _).
%total {} (id/mtm_pair_inv _ _ _).

expand_respects_id : id/rtm R R'
		      -> id/mtm M M'
		      -> expand A R M
		      -> expand A R' M'
		      -> type.
%mode expand_respects_id +X1 +X2 +X3 -X4.

- : expand_respects_id _ _ D D.

%worlds (rtm_block) (expand_respects_id _ _ _ _).
%total {} (expand_respects_id _ _ _ _).
%reduces D1 = D2 (expand_respects_id _ _ D2 D1).

canon_respects_id :  id/mtm M M'
		     -> id/tp A A'
		     -> canon M A
		     -> canon M' A'
		     -> type.
%mode canon_respects_id +X1 +X2 +X3 -X4.

- : canon_respects_id _ _ D D.

%worlds (atom_block) (canon_respects_id _ _ _ _).
%total {} (canon_respects_id _ _ _ _).
%reduces D1 = D2 (canon_respects_id _ _ D2 D1).

hsubst_m_respects_id : id/mtm M2 M2'
			-> id/tp A2 A2'
			-> ({x} id/mtm (M x) (M' x))
			-> hsubst_m M2 A2 M Ms
			-> hsubst_m M2' A2' M' Ms
			-> type.
%mode hsubst_m_respects_id +X1 +X2 +X3 +X4 -X5.

- : hsubst_m_respects_id _ _ _ D D.

%worlds (rtm_block) (hsubst_m_respects_id _ _ _ _ _).
%total {} (hsubst_m_respects_id _ _ _ _ _).
%reduces D1 = D2 (hsubst_m_respects_id _ _ _ D2 D1).

id/mtm_asm_cong : id/rtm R R'
		   -> id/mtm (asm R) (asm R')
		   -> type.
%mode id/mtm_asm_cong +X1  -X3.

- : id/mtm_asm_cong _ id/mtm_refl.

%worlds (rtm_block) (id/mtm_asm_cong _ _).
%total {} (id/mtm_asm_cong _ _).

false : type.
%freeze false.

hsubst_rr_closed_contra : hsubst_rr M2 A2 ([_] R) M' A'
                           -> false
                           -> type.
%mode hsubst_rr_closed_contra +X1 -X2.

- : hsubst_rr_closed_contra 
     (hsubst_rr_app _ _ Dr)
     X
     <- hsubst_rr_closed_contra Dr X.

- : hsubst_rr_closed_contra 
     (hsubst_rr_fst D)
     X
     <- hsubst_rr_closed_contra D X.

- : hsubst_rr_closed_contra 
     (hsubst_rr_snd D)
     X
     <- hsubst_rr_closed_contra D X.

%worlds (rtm_block) (hsubst_rr_closed_contra _ _).
%total D (hsubst_rr_closed_contra D _).

%% contradiction of root and non-root

hsubst_r_rr_contra : hsubst_r M2 A2 R R'
                      -> hsubst_rr M2 A2 R M' A'
                      -> false
                      -> type.
%mode hsubst_r_rr_contra +X1 +X2 -X3.

- : hsubst_r_rr_contra
     hsubst_r_closed
     Drr
     X
     <- hsubst_rr_closed_contra Drr X.

- : hsubst_r_rr_contra 
     (hsubst_r_app _ DsrR)
     (hsubst_rr_app _ _ DsrrR)
     X
     <- hsubst_r_rr_contra DsrR DsrrR X.

- : hsubst_r_rr_contra 
     (hsubst_r_fst DsrR)
     (hsubst_rr_fst DsrrR)
     X
     <- hsubst_r_rr_contra DsrR DsrrR X.

- : hsubst_r_rr_contra 
     (hsubst_r_snd DsrR)
     (hsubst_rr_snd DsrrR)
     X
     <- hsubst_r_rr_contra DsrR DsrrR X.

%worlds (rtm_block) (hsubst_r_rr_contra _ _ _). %% bar in extra block for lemma below's future use
%total (D) (hsubst_r_rr_contra D _ _).

%% false implies id
false_implies_id/mtm : {M} {M'}
                        false 
                        -> id/mtm M M'
                        -> type.
%mode false_implies_id/mtm +X1 +X2 +X3 -X4.
%worlds (rtm_block) (false_implies_id/mtm _ _ _ _). %% bar in extra block for lemma below's future use
%total {} (false_implies_id/mtm _ _ _ _).

hsubst_r_vacuous_id : hsubst_r M2 A2 ([_] R) R'
                     -> id/rtm R' R
                     -> type.
%mode hsubst_r_vacuous_id +X1 -X2.

hsubst_m_vacuous_id : hsubst_m M2 A2 ([_] M) M'
                     -> id/mtm M' M
                     -> type.
%mode hsubst_m_vacuous_id +X1 -X2.

%% R

- : hsubst_r_vacuous_id hsubst_r_closed id/rtm_refl.

- : hsubst_r_vacuous_id (hsubst_r_app Dm Dr) Did'
     <- hsubst_r_vacuous_id Dr DidR
     <- hsubst_m_vacuous_id Dm DidM
     <- id/rtm_app_cong DidR DidM Did'.

- : hsubst_r_vacuous_id (hsubst_r_fst D) Did'
     <- hsubst_r_vacuous_id D Did
     <- id/rtm_fst_cong Did Did'.

- : hsubst_r_vacuous_id (hsubst_r_snd D) Did'
     <- hsubst_r_vacuous_id D Did
     <- id/rtm_snd_cong Did Did'.

%% M

- : hsubst_m_vacuous_id
     (hsubst_m_r Dr)
     Did'
     <- hsubst_r_vacuous_id Dr Did
     <- id/mtm_asm_cong Did Did'.

- : hsubst_m_vacuous_id
     (hsubst_m_rr D)
     Did
     <- hsubst_rr_closed_contra D X
     <- false_implies_id/mtm _ _ X Did.

- : hsubst_m_vacuous_id
     (hsubst_m_lam D)
     Did'
     <- ({x} 
           hsubst_m_vacuous_id (D x) (Did x))
     <- id/mtm_lam_cong Did Did'.

- : hsubst_m_vacuous_id
     (hsubst_m_pair D2 D1)
     Did'
     <- hsubst_m_vacuous_id D1 Did1
     <- hsubst_m_vacuous_id D2 Did2
     <- id/mtm_pair_cong Did1 Did2 Did'.

%worlds (rtm_block) (hsubst_r_vacuous_id _ _) (hsubst_m_vacuous_id _ _).
%total (D1 D2) 
(hsubst_r_vacuous_id D1 _)
(hsubst_m_vacuous_id D2 _).

hsubst_m_unique : hsubst_m M2 A2 M M'
                   -> hsubst_m M2 A2 M M''
                   -> id/mtm M' M''
                   -> type.
%mode hsubst_m_unique +X1 +X2 -X3.

hsubst_r_unique : hsubst_r M2 A2 R R'
                   -> hsubst_r M2 A2 R R''
                   -> id/rtm R' R''
                   -> type.
%mode hsubst_r_unique +X1 +X2 -X3.

hsubst_rr_unique : hsubst_rr M2 A2 R M' A'
                    -> hsubst_rr M2 A2 R M'' A''
                    -> id/mtm M' M''
                    -> id/tp A' A''
                    -> type.
%mode hsubst_rr_unique +X1 +X2 -X3 -X4.

%% M

- : hsubst_m_unique
     (hsubst_m_r Dsr)
     (hsubst_m_r Dsr')
     DidAsm
     <- hsubst_r_unique Dsr Dsr' DidR
     <- id/mtm_asm_cong DidR DidAsm.

- : hsubst_m_unique
     (hsubst_m_rr Dsr)
     (hsubst_m_rr Dsr')
     Did
     <- hsubst_rr_unique Dsr Dsr' Did _.

%% contradict mismatch
- : hsubst_m_unique
     (hsubst_m_r Dsr)
     (hsubst_m_rr Dsrr)
     Did
     <- hsubst_r_rr_contra Dsr Dsrr X
     <- false_implies_id/mtm _ _ X Did.

%% contradict mismatch
- : hsubst_m_unique
     (hsubst_m_rr Dsrr)
     (hsubst_m_r Dsr)
     Did
     <- hsubst_r_rr_contra Dsr Dsrr X
     <- false_implies_id/mtm _ _ X Did.

- : hsubst_m_unique
     (hsubst_m_pair DsRight DsLeft)
     (hsubst_m_pair DsRight' DsLeft')
     DidPair
     <- hsubst_m_unique DsLeft DsLeft' DidLeft
     <- hsubst_m_unique DsRight DsRight' DidRight
     <- id/mtm_pair_cong DidLeft DidRight DidPair.

- : hsubst_m_unique
     (hsubst_m_lam Ds)
     (hsubst_m_lam Ds')
     DidLam
     <- ({y:rtm} hsubst_m_unique (Ds y) (Ds' y) (Did y))
     <- id/mtm_lam_cong Did DidLam.
     
%% R non-root

- : hsubst_r_unique D D id/rtm_refl.

- : hsubst_r_unique 
     (hsubst_r_closed : hsubst_r M2 A2 ([_] R) R)
     (D : hsubst_r M2 A2 ([_] R) R')
     Did'
     <- hsubst_r_vacuous_id D Did
     <- id/rtm_sym Did Did'.

- : hsubst_r_unique 
     (D : hsubst_r M2 A2 ([_] R) R')
     (hsubst_r_closed : hsubst_r M2 A2 ([_] R) R)
     Did
     <- hsubst_r_vacuous_id D Did.

- : hsubst_r_unique 
     (hsubst_r_app DsM' DsR') 
     (hsubst_r_app DsM'' DsR'')
     DidApp
     <- hsubst_r_unique DsR' DsR'' DidR
     <- hsubst_m_unique DsM' DsM'' DidM
     <- id/rtm_app_cong DidR DidM DidApp.

- : hsubst_r_unique
     (hsubst_r_fst DsR')
     (hsubst_r_fst DsR'')
     DidFst
     <- hsubst_r_unique DsR' DsR'' DidR
     <- id/rtm_fst_cong DidR DidFst.
- : hsubst_r_unique
     (hsubst_r_snd DsR')
     (hsubst_r_snd DsR'')
     DidSnd
     <- hsubst_r_unique DsR' DsR'' DidR
     <- id/rtm_snd_cong DidR DidSnd.

%% R root

- : hsubst_rr_unique 
     hsubst_rr_var
     hsubst_rr_var
     id/mtm_refl
     id/tp_refl.

- : hsubst_rr_unique
     (hsubst_rr_app DsM4' DsM3 DsR1)
     (hsubst_rr_app DsM4'-2 DsM3-2 DsR1-2)
     DidM4''
     DidA4
     <- hsubst_rr_unique DsR1 DsR1-2 DidLam DidArrow
     <- hsubst_m_unique DsM3 DsM3-2 DidM3'
     <- id/tp_arrow_inv DidArrow DidA3 DidA4
     <- id/mtm_lam_inv DidLam DidM4'
     <- hsubst_m_respects_id DidM3' DidA3 DidM4' DsM4' DsM4'-1
     <- hsubst_m_unique DsM4'-1 DsM4'-2 DidM4''.

- : hsubst_rr_unique 
     (hsubst_rr_fst DsR')
     (hsubst_rr_fst DsR'')
     DidMl
     DidAl
     <- hsubst_rr_unique DsR' DsR'' DidPair DidProd
     <- id/tp_prod_inv DidProd DidAl _
     <- id/mtm_pair_inv DidPair DidMl _.

- : hsubst_rr_unique 
     (hsubst_rr_snd DsR')
     (hsubst_rr_snd DsR'')
     DidMr
     DidAr
     <- hsubst_rr_unique DsR' DsR'' DidPair DidProd
     <- id/tp_prod_inv DidProd _ DidAr
     <- id/mtm_pair_inv DidPair _ DidMr.

%worlds (rtm_block) 
(hsubst_m_unique _ _ _)
(hsubst_r_unique _ _ _)
(hsubst_rr_unique _ _ _ _).

%total (D1 D2 D3) 
(hsubst_r_unique D2 _ _)
(hsubst_rr_unique D3 _ _ _)
(hsubst_m_unique D1 _ _).

expand_exists : {A}
                 atom R A
                 -> expand A R M
                 -> canon M A
                 -> type.
%mode expand_exists +X0 +X1 -X2 -X3.

- : expand_exists 
     b
     D
     expand_b
     (canon_asm D).

- : expand_exists
     (arrow A2 A)
     DaR
     (expand_arrow DeApp DeX)
     (canon_lam DcApp)
     <- ({x : rtm}
           {dx : atom x A2}
           expand_exists A2 dx (DeX x) (DcM x dx))
     <- ({x : rtm}
           {dx : atom x A2}
           expand_exists A (atom_app (DcM x dx) DaR) (DeApp x) (DcApp x dx)).

- : expand_exists
     (prod A1 A2)
     DaR
     (expand_prod DeS DeF)
     (canon_pair DcS DcF)
     <- expand_exists A1 (atom_fst DaR) DeF DcF
     <- expand_exists A2 (atom_snd DaR) DeS DcS.

%worlds (atom_block) (expand_exists _ _ _ _). 
%total D (expand_exists D _ _ _).

expand_unique : expand A R M 
                 -> expand A R M'
                 -> id/mtm M M'
                 -> type.
%mode expand_unique +X1 +X2 -X3.

- : expand_unique
     expand_b
     expand_b
     id/mtm_refl.

- : expand_unique 
     (expand_arrow 
        (DeApp : {x : rtm} expand A (app R (Mx x)) (MApp x))
        (DeX : {x : rtm} expand A2 x (Mx x)))
      (expand_arrow 
         (DeApp' : {x : rtm} expand A (app R (Mx' x)) (MApp' x))
         (DeX' : {x : rtm} expand A2 x (Mx' x)))
     DidLam
     <- ({x : rtm}
           expand_unique (DeX x) (DeX' x) (DidX x))
     <- ({x : rtm}
           id/rtm_app_cong (id/rtm_refl : id/rtm R R) (DidX x) (DidApp x))
     <- ({x : rtm}
           expand_respects_id (DidApp x) id/mtm_refl (DeApp x) (DeApp-2 x))
     <- ({x : rtm} 
           expand_unique (DeApp-2 x) (DeApp' x) (DidAppExp x))
     <- id/mtm_lam_cong DidAppExp DidLam.

- : expand_unique
     (expand_prod DeS DeF)
     (expand_prod DeS' DeF')
     DidPair
     <- expand_unique DeF DeF' DidF
     <- expand_unique DeS DeS' DidS
     <- id/mtm_pair_cong DidF DidS DidPair.
     
%worlds (rtm_block) (expand_unique _ _ _).
%total D (expand_unique _ D _).