Require pr0_gen.
Require pr0_subst1.
Require pr2_defs.
+Require pr2_gen.
Require pr2_subst1.
Section pr2_gen_context. (************************************************)
(EX x2 | (subst1 d u t2 (lift (1) d x2)) &
(pr2 a x1 x2)
).
- Intros until 1; XElim H; Intros.
-(* case 1: pr2_pr0 *)
- Pr0Subst1; Pr0Gen; Rewrite H in H3; Clear H x; XEAuto.
+ Intros until 1; XElim H; Intros;
+ Pr0Subst1; Pr0Gen.
+(* case 1: pr2_free *)
+ Rewrite H in H3; Clear H x; XEAuto.
(* case 2: pr2_delta *)
+ Rewrite H0 in H5; Clear H0 x.
Apply (lt_eq_gt_e i d0); Intros.
(* case 2.1: i < d0 *)
Subst1Confluence; CSubst1Drop.
Rewrite minus_x_Sy in H; [ Idtac | XAuto ].
- CSubst1GenBase; Rewrite H in H6; Clear H x0.
- Rewrite (lt_plus_minus i d0) in H3; [ Idtac | XAuto ].
- DropDis; Rewrite H in H7; Clear H x2.
+ CSubst1GenBase; Rewrite H in H7; Clear H x2.
+ Rewrite (lt_plus_minus i d0) in H4; [ Idtac | XAuto ].
+ DropDis; Rewrite H in H8; Clear H x3.
Subst1Subst1; Pattern 2 d0 in H; Rewrite (lt_plus_minus i d0) in H; [ Idtac | XAuto ].
- Subst1Gen; Rewrite H in H9; Simpl in H9; Clear H x2.
- Rewrite <- lt_plus_minus in H9; [ Idtac | XAuto ].
- Rewrite <- lt_plus_minus_r in H9; XEAuto.
+ Subst1Gen; Rewrite H in H10; Simpl in H10; Clear H x3.
+ Rewrite <- lt_plus_minus in H10; [ Idtac | XAuto ].
+ Rewrite <- lt_plus_minus_r in H10; XEAuto.
(* case 2.2: i = d0 *)
- Rewrite H5 in H; Rewrite H5 in H0; Clear H5 i.
- DropDis; Inversion H; Rewrite <- H7 in H0; Rewrite <- H7 in H1; Rewrite <- H7; Clear H H6 H7 e u.
+ Rewrite H0 in H; Rewrite H0 in H1; Clear H0 i.
+ DropDis; Inversion H; Rewrite <- H8 in H1; Rewrite <- H8 in H2; Rewrite <- H8; Clear H H7 H8 e u.
Subst1Confluence; Subst1Gen; Rewrite H0 in H; Clear H0 x; XEAuto.
(* case 2.3: i > d0 *)
- Subst1Confluence; Subst1Gen; Rewrite H4 in H0; Clear H1 H4 x.
+ Subst1Confluence; Subst1Gen; Rewrite H5 in H1; Clear H2 H5 x.
CSubst1Drop; DropDis; XEAuto.
Qed.