Section pc3_gen. (********************************************************)
Theorem pc3_gen_sort: (c:?; m,n:?) (pc3 c (TSort m) (TSort n)) -> m = n.
- Intros; Pc3Confluence; Repeat Pr3GenBase.
- Rewrite H in H0; Clear H x c.
- Inversion H0; XAuto.
+ Intros; Pc3Unfold; Repeat Pr3GenBase.
+ Rewrite H0 in H; Clear H0 x c.
+ TGenBase; XAuto.
Qed.
Theorem pc3_gen_abst: (c:?; u1,u2,t1,t2:?)
(pc3 c u1 u2) /\
(b:?; u:?) (pc3 (CTail c (Bind b) u) t1 t2).
Intros.
- Pc3Confluence; Repeat Pr3GenBase; Rewrite H0 in H1; Clear H0 x.
- Inversion H1; Rewrite H0 in H4; Rewrite H6 in H5.
+ Pc3Unfold; Repeat Pr3GenBase; Rewrite H1 in H; Clear H1 x.
+ TGenBase; Rewrite H1 in H4; Rewrite H6 in H5.
XEAuto.
Qed.
(e:?) (drop h d c e) ->
(pc3 e t1 t2).
Intros.
- Pc3Confluence; Repeat Pr3Gen; Rewrite H2 in H1; Clear H2 x.
- LiftGen; Rewrite H in H3; XEAuto.
+ Pc3Unfold; Repeat Pr3Gen; Rewrite H2 in H; Clear H2 x.
+ LiftGen; Rewrite H in H4; XEAuto.
Qed.
Theorem pc3_gen_not_abst: (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
(lift (1) (0) (TTail (Bind Abst) u2 t2))
).
XElim b; Intros;
- Try EqFalse; Pc3Confluence; Repeat Pr3Gen;
- Try (Rewrite H3 in H0; TGenBase);
- Rewrite H0 in H2; Clear H H0 x;
+ Try EqFalse; Pc3Unfold; Repeat Pr3Gen;
+ Try (Rewrite H0 in H3; TGenBase);
+ Rewrite H1 in H0; Clear H H1 x;
EApply pc3_pr3_t; XEAuto.
Qed.
Theorem pc3_gen_lift_abst: (c:?; t,t2,u2:?; h,d:?)
(pc3 c (lift h d t)
- (TTail (Bind Abst) u2 t2)
+ (TTail (Bind Abst) u2 t2)
) ->
(e:?) (drop h d c e) ->
(EX u1 t1 | (pr3 e t (TTail (Bind Abst) u1 t1)) &
(b:B; u:T)(pr3 (CTail c (Bind b) u) t2 (lift h (S d) t1))
).
Intros.
- Pc3Confluence; Repeat Pr3Gen; Rewrite H in H2; Clear H x.
+ Pc3Unfold; Repeat Pr3Gen; Rewrite H1 in H; Clear H1 x.
LiftGenBase; Rewrite H in H3; Rewrite H1 in H4; Rewrite H2 in H5; XEAuto.
Qed.
_: (drop ?2 ?3 ?1 ?7) |- ? ] ->
LApply (pc3_gen_lift_abst ?1 ?4 ?6 ?5 ?2 ?3); [ Intros H_x | XAuto ];
LApply (H_x ?7); [ Clear H_x; Intros H_x | XAuto ];
- XElim H_x; Intros.
+ XElim H_x; Intros
+ | _ -> Pr3Gen.