+ Section pr3_gen_base. (***************************************************)
+
+ Theorem pr3_gen_sort: (c:?; x:?; n:?) (pr3 c (TSort n) x) ->
+ x = (TSort n).
+ Intros; InsertEq H '(TSort n); XElim H; Clear y x; Intros.
+(* case 1: pr3_refl *)
+ XAuto.
+(* case 2: pr3_sing *)
+ Rewrite H2 in H; Clear H2 t1; Pr2GenBase; XAuto.
+ Qed.
+
+ Tactic Definition IH :=
+ Match Context With
+ | [ H: (u,t:T) (TTail (Bind Abst) ?1 ?2) = (TTail (Bind Abst) u t) -> ? |- ? ] ->
+ LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
+ XDecompose H
+ | [ H: (u,t:T) (TTail (Flat Appl) ?1 ?2) = (TTail (Flat Appl) u t) -> ? |- ? ] ->
+ LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
+ XDecompose H
+ | [ H: (u,t:T) (TTail (Flat Cast) ?1 ?2) = (TTail (Flat Cast) u t) -> ? |- ? ] ->
+ LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
+ XDecompose H.
+
+ Theorem pr3_gen_abst: (c:?; u1,t1,x:?)
+ (pr3 c (TTail (Bind Abst) u1 t1) x) ->
+ (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
+ (pr3 c u1 u2) & (b:?; u:?)
+ (pr3 (CTail c (Bind b) u) t1 t2)
+ ).
+ Intros until 1; InsertEq H '(TTail (Bind Abst) u1 t1);
+ UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
+ Rename x into u0; Rename x0 into t0.
+(* case 1 : pr3_refl *)
+ XEAuto.
+(* case 2 : pr3_sing *)
+ Rewrite H2 in H; Clear H0 H2 t1; Pr2GenBase.
+ Rewrite H0 in H1; Clear H0 t2; IH; XEAuto.
+ Qed.
+
+ Theorem pr3_gen_appl: (c:?; u1,t1,x:?)
+ (pr3 c (TTail (Flat Appl) u1 t1) x) -> (OR
+ (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
+ (pr3 c u1 u2) & (pr3 c t1 t2)
+ ) |
+ (EX y1 z1 u2 t2 | (pr3 c (TTail (Bind Abbr) u2 t2) x) &
+ (pr3 c u1 u2) &
+ (pr3 c t1 (TTail (Bind Abst) y1 z1)) &
+ (b:?; u:?) (pr3 (CTail c (Bind b) u) z1 t2)
+ ) |
+ (EX b y1 z1 z2 u2 v2 t2 |
+ (pr3 c (TTail (Bind b) v2 z2) x) & ~b=Abst &
+ (pr3 c u1 u2) &
+ (pr3 c t1 (TTail (Bind b) y1 z1)) &
+ (pr3 c y1 v2) & (pr0 z1 t2))
+ ).
+ Intros; InsertEq H '(TTail (Flat Appl) u1 t1).
+ UnIntro t1 H; UnIntro u1 H.
+ XElim H; Clear y x; Intros;
+ Rename x into u0; Rename x0 into t0.
+(* case 1: pr3_refl *)
+ XEAuto.
+(* case 2: pr3_sing *)
+ Rewrite H2 in H; Clear H2 t1; Pr2GenBase.
+(* case 2.1: short step: compatibility *)
+ Rewrite H3 in H1; Clear H0 H3 t2.
+ IH; Try (Rewrite H0; Clear H0 t3); XDEAuto 6.
+(* case 2.2: short step: beta *)
+ Rewrite H4 in H0; Rewrite H3; Clear H1 H3 H4 t0 t2; XEAuto.
+(* case 2.3: short step: upsilon *)
+ Rewrite H5 in H0; Rewrite H4; Clear H1 H4 H5 t0 t2; XEAuto.
+ Qed.
+
+ Theorem pr3_gen_cast: (c:?; u1,t1,x:?)
+ (pr3 c (TTail (Flat Cast) u1 t1) x) ->
+ (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
+ (pr3 c u1 u2) & (pr3 c t1 t2)
+ ) \/
+ (pr3 c t1 x).
+ Intros; InsertEq H '(TTail (Flat Cast) u1 t1);
+ UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
+ Rename x into u0; Rename x0 into t0.
+(* case 1: pr3_refl *)
+ Rewrite H; Clear H t; XEAuto.
+(* case 2: pr3_sing *)
+ Rewrite H2 in H; Clear H2 t1; Pr2GenBase.
+(* case 2.1: short step: compatinility *)
+ Rewrite H3 in H1; Clear H0 H3 t2;
+ IH; Try Rewrite H0; XEAuto.
+(* case 2.2: short step: epsilon *)
+ XEAuto.
+ Qed.
+
+ End pr3_gen_base.
+
+ Tactic Definition Pr3GenBase :=
+ Match Context With
+ | [ H: (pr3 ?1 (TSort ?2) ?3) |- ? ] ->
+ LApply (pr3_gen_sort ?1 ?3 ?2); [ Clear H; Intros | XAuto ]
+ | [ H: (pr3 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
+ LApply (pr3_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XDecompose H
+ | [ H: (pr3 ?1 (TTail (Flat Appl) ?2 ?3) ?4) |- ? ] ->
+ LApply (pr3_gen_appl ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XDecompose H
+ | [ H: (pr3 ?1 (TTail (Flat Cast) ?2 ?3) ?4) |- ? ] ->
+ LApply (pr3_gen_cast ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XDecompose H.
+