(*#* #start file *)
-(*#* #caption "confluence with substitution" *)
-(*#* #cap #cap t1,t2,v1,v2 #alpha w1 in U1, w2 in U2 *)
+(*#* #caption "confluence with strict substitution" *)
+(*#* #cap #cap t1, t2 #alpha v1 in W1, v2 in W2, w1 in U1, w2 in U2 *)
Theorem pr0_subst0: (t1,t2:?) (pr0 t1 t2) ->
(v1,w1:?; i:?) (subst0 i v1 t1 w1) ->
(* case 3: pr0_beta *)
Repeat Subst0Gen; Rewrite H3; Try Rewrite H5; Try Rewrite H6;
Repeat IH; XEAuto.
-(* case 4: pr0_gamma *)
+(* case 4: pr0_upsilon *)
Repeat Subst0Gen; Rewrite H6; Try Rewrite H8; Try Rewrite H9;
Repeat IH; XDEAuto 7.
(* case 5: pr0_delta *)
LApply (H1 ?4 ?5 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
LApply (H1 ?4); [ Clear H1; Intros H1 | XAuto ];
XElim H1; [ Intros | Intros H1; XElim H1; Intros ]
- | [ H1: (subst0 ?0 ?1 ?2 ?3); H2: (pr0 ?4 ?1) |- ? ] ->
- LApply (pr0_subst0_back ?1 ?2 ?3 ?0); [ Clear H1; Intros H1 | XAuto ];
- LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
- XElim H1; Intros
+ | [ _: (subst0 ?0 ?1 ?2 ?3); _: (pr0 ?4 ?1) |- ? ] ->
+ LApply (pr0_subst0_back ?1 ?2 ?3 ?0); [ Intros H_x | XAuto ];
+ LApply (H_x ?4); [ Clear H_x; Intros H_x | XAuto ];
+ XElim H_x; Intros
| [ H1: (subst0 ?0 ?1 ?2 ?3); H2: (pr0 ?1 ?4) |- ? ] ->
LApply (pr0_subst0_fwd ?1 ?2 ?3 ?0); [ Clear H1; Intros H1 | XAuto ];
LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];