- CSubst0Drop; Apply pc3_pr3_u2 with t0 := t1; XEAuto.
-(* case 2.3.2 : i < i0, csubst0_fst *)
- Inversion H; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H H8 H9 H10 c2 t2 x0 x1 x2.
- Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
- Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
-(* case 2.3.3: i < i0, csubst0_snd *)
- Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3.
- CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
-(* case 2.3.4: i < i0, csubst0_both *)
- Inversion H; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H H9 H10 H11 c2 t2 x0 x1 x3.
+ CSubst0Drop; Apply pc3_pr2_u2 with t0 := t1; XEAuto.
+(* case 2.3.2 : i < i0, csubst0_snd *)
+ CGenBase; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H7; Clear H9 H10 H11 c2 t3 x0 x1 x2.