9 Section pr0_gen_abbr. (***************************************************)
11 Theorem pr0_gen_abbr : (u1,t1,x:?) (pr0 (TTail (Bind Abbr) u1 t1) x) ->
12 (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
15 (EX y | (pr0 t1 y) & (subst0 (0) u2 y t2))
17 (pr0 t1 (lift (1) (0) x)).
19 Inversion H; Clear H; XDEAuto 6.
24 Section pr0_gen_void. (***************************************************)
26 Theorem pr0_gen_void : (u1,t1,x:?) (pr0 (TTail (Bind Void) u1 t1) x) ->
27 (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
28 (pr0 u1 u2) & (pr0 t1 t2)
30 (pr0 t1 (lift (1) (0) x)).
32 Inversion H; Clear H; XEAuto.
37 Section pr0_gen_lift. (***************************************************)
39 Tactic Definition IH :=
41 | [ H: (_:?; _:?) ?0 = (lift ? ? ?) -> ?;
42 H0: ?0 = (lift ? ?2 ?3) |- ? ] ->
43 LApply (H ?3 ?2); [ Clear H H0; Intros H_x | XAuto ];
44 XElim H_x; Intro; Intros H_x; Intro;
45 Try Rewrite H_x; Try Rewrite H_x in H3; Clear H_x.
47 (*#* #caption "generation lemma for lift" *)
48 (*#* #cap #alpha t1 in U1, t2 in U2, x in T, d in i *)
50 Theorem pr0_gen_lift : (t1,x:?; h,d:?) (pr0 (lift h d t1) x) ->
51 (EX t2 | x = (lift h d t2) & (pr0 t1 t2)).
52 Intros until 1; InsertEq H '(lift h d t1);
53 UnIntro H d; UnIntro H t1; XElim H; Clear y x; Intros;
54 Rename x into t3; Rename x0 into d.
58 NewInduction k; LiftGen; Rewrite H3; Clear H3 t0;
60 (* case 3 : pr0_beta *)
61 LiftGen; Rewrite H3; Clear H3 t0.
62 LiftGen; Rewrite H3; Clear H3 H5 x1 k.
64 (* case 4 : pr0_upsilon *)
65 LiftGen; Rewrite H6; Clear H6 t0.
66 LiftGen; Rewrite H6; Clear H6 x1.
68 Rewrite <- lift_d; [ Simpl | XAuto ].
69 Rewrite <- lift_flat; XEAuto.
70 (* case 5 : pr0_delta *)
71 LiftGen; Rewrite H4; Clear H4 t0.
72 IH; IH; Arith3In H3 d; Subst0Gen.
74 (* case 6 : pr0_zeta *)
75 LiftGen; Rewrite H2; Clear H2 t0.
76 Arith7In H4 d; LiftGen; Rewrite H2; Clear H2 x1.
78 (* case 7 : pr0_zeta *)
79 LiftGen; Rewrite H1; Clear H1 t0.
85 Tactic Definition Pr0Gen :=
87 | [ H: (pr0 (TTail (Bind Abbr) ?1 ?2) ?3) |- ? ] ->
88 LApply (pr0_gen_abbr ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
90 [ Intros H; XElim H; Do 4 Intro; Intros H_x;
91 XElim H_x; [ Intros | Intros H_x; XElim H_x; Intros ]
93 | [ H: (pr0 (TTail (Bind Void) ?1 ?2) ?3) |- ? ] ->
94 LApply (pr0_gen_void ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
95 XElim H; [ Intros H; XElim H; Intros | Intros ]
96 | [ H: (pr0 (lift ?0 ?1 ?2) ?3) |- ? ] ->
97 LApply (pr0_gen_lift ?2 ?3 ?0 ?1); [ Clear H; Intros H | XAuto ];