Require drop_props.
Require csubst0_defs.
+Require fsubst0_defs.
Require pc3_props.
Require pc3_subst0.
Require ty0_defs.
+Require ty0_gen.
Require ty0_lift.
Require ty0_props.
Intros until 1; XElim H.
(* case 1: ty0_conv *)
Intros until 6; XElim H4; Intros.
-(* case 1.1: fsubst0_t *)
+(* case 1.1: fsubst0_snd *)
IHT; EApply ty0_conv; XEAuto.
-(* case 1.2: fsubst0_c *)
+(* case 1.2: fsubst0_fst *)
IHC; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
-(* case 1.3: fsubst0_b *)
+(* case 1.3: fsubst0_both *)
IHCT; IHCT; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
(* case 2: ty0_sort *)
Intros until 2; XElim H0; Intros.
-(* case 2.1: fsubst0_t *)
+(* case 2.1: fsubst0_snd *)
Subst0GenBase.
-(* case 2.2: fsubst0_c *)
+(* case 2.2: fsubst0_fst *)
XAuto.
-(* case 2.3: fsubst0_b *)
+(* case 2.3: fsubst0_both *)
Subst0GenBase.
(* case 3: ty0_abbr *)
Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
-(* case 3.1: fsubst0_t *)
+(* case 3.1: fsubst0_snd *)
Subst0GenBase; Rewrite H6; Rewrite <- H3 in H5; Clear H3 H6 i t3.
DropDis; Inversion H5; Rewrite <- H6 in H0; Rewrite H7 in H1; XEAuto.
-(* case 3.2: fsubst0_c *)
+(* case 3.2: fsubst0_fst *)
Apply (lt_le_e n i); Intros; CSubst0Drop.
(* case 3.2.1: n < i, none *)
EApply ty0_abbr; XEAuto.
-(* case 3.2.2: n < i, csubst0_fst *)
+(* case 3.2.2: n < i, csubst0_snd *)
Inversion H0; CSubst0Drop.
Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8;
Clear H0 H10 H11 H12 x0 x1 x2.
DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
IHT; EApply ty0_abbr; XEAuto.
-(* case 3.2.3: n < i, csubst0_snd *)
+(* case 3.2.3: n < i, csubst0_fst *)
Inversion H0; CSubst0Drop.
Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7;
Clear H0 H10 H11 H12 x0 x1 x3.
IHCT; EApply ty0_abbr; XEAuto.
(* case 3.2.5: n >= i *)
EApply ty0_abbr; XEAuto.
-(* case 3.3: fsubst0_b *)
+(* case 3.3: fsubst0_both *)
Subst0GenBase; Rewrite H7; Rewrite <- H3 in H4; Rewrite <- H3 in H6; Clear H3 H7 i t3.
DropDis; Inversion H6; Rewrite <- H7 in H0; Rewrite H8 in H1.
CSubst0Drop; XEAuto.
(* case 4: ty0_abst *)
Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
-(* case 4.1: fsubst0_t *)
+(* case 4.1: fsubst0_snd *)
Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
-(* case 4.2: fsubst0_c *)
+(* case 4.2: fsubst0_fst *)
Apply (lt_le_e n i); Intros; CSubst0Drop.
(* case 4.2.1: n < i, none *)
EApply ty0_abst; XEAuto.
-(* case 4.2.2: n < i, csubst0_fst *)
+(* case 4.2.2: n < i, csubst0_snd *)
Inversion H0; CSubst0Drop.
Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8; Rewrite <- H12;
Clear H0 H10 H11 H12 x0 x1 x2.
DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
IHT; EApply ty0_conv;
[ EApply ty0_lift | EApply ty0_abst | EApply pc3_lift ]; XEAuto.
-(* case 4.2.3: n < i, csubst0_snd *)
+(* case 4.2.3: n < i, csubst0_fst *)
Inversion H0; CSubst0Drop.
Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Rewrite <- H12;
Clear H0 H10 H11 H12 x0 x1 x3.
]; XEAuto.
(* case 4.2.4: n >= i *)
EApply ty0_abst; XEAuto.
-(* case 4.3: fsubst0_b *)
+(* case 4.3: fsubst0_both *)
Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
(* case 5: ty0_bind *)
Intros until 7; XElim H5; Intros; Clear H4.
-(* case 5.1: fsubst0_t *)
+(* case 5.1: fsubst0_snd *)
Subst0GenBase; Rewrite H4; Clear H4 t6.
(* case 5.1.1: subst0 on left argument *)
Ty0Correct; IHT; IHTb1; Ty0Correct.
Ty0Correct; IHT; IHTb1; IHTTb; Ty0Correct.
EApply ty0_conv;
[ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
-(* case 5.2: fsubst0_c *)
+(* case 5.2: fsubst0_fst *)
IHC; IHCb; Ty0Correct; EApply ty0_bind; XEAuto.
-(* case 5.3: fsubst0_b *)
+(* case 5.3: fsubst0_both *)
Subst0GenBase; Rewrite H4; Clear H4 t6.
(* case 5.3.1: subst0 on left argument *)
IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTb1; Ty0Correct.
| EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
(* case 6: ty0_appl *)
Intros until 5; XElim H3; Intros.
-(* case 6.1: fsubst0_t *)
+(* case 6.1: fsubst0_snd *)
Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
(* case 6.1.1: subst0 on left argument *)
Ty0Correct; Ty0GenBase; IHT; Ty0Correct.
Ty0Correct; Ty0GenBase; Move H after H10; Ty0Correct; IHT; Clear H2; IHT.
EApply ty0_conv;
[ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
-(* case 6.2: fsubst0_c *)
+(* case 6.2: fsubst0_fst *)
IHC; Clear H2; IHC; EApply ty0_appl; XEAuto.
-(* case 6.3: fsubst0_b *)
+(* case 6.3: fsubst0_both *)
Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
(* case 6.3.1: subst0 on left argument *)
IHC; Ty0Correct; Ty0GenBase; Clear H2; IHC; IHCT.
| EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
(* case 7: ty0_cast *)
Clear c1 t t1; Intros until 5; XElim H3; Intros; Clear c2 t3.
-(* case 7.1: fsubst0_t *)
+(* case 7.1: fsubst0_snd *)
Subst0GenBase; Rewrite H3; Clear H3 t4.
(* case 7.1.1: subst0 on left argument *)
IHT; EApply ty0_conv;
[ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
| Idtac ]
| EApply pc3_fsubst0 ]; XEAuto.
-(* case 7.2: fsubst0_c *)
+(* case 7.2: fsubst0_fst *)
IHC; Clear H2; IHC; EApply ty0_cast; XEAuto.
-(* case 6.3: fsubst0_b *)
+(* case 6.3: fsubst0_both *)
Subst0GenBase; Rewrite H3; Clear H3 t4.
(* case 7.3.1: subst0 on left argument *)
IHC; IHCT; Clear H2; IHC.
End ty0_fsubst0.
Hints Resolve ty0_subst0 : ltlc.
-