- first piece of the mutual induction for preservation finally closed!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reducibility / tpr_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma
index b4d76066affbb8af45839e6fa16b90455c4474a1..8d6b0363a87dd5412d1c930dedceafb935febf0d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_lift.ma
@@ -77,7 +77,7 @@ lemma tpr_inv_lift1: t_deliftable_sn tpr.
   elim (IHV12 … HWV1) -V1 #W2 #HWV2 #HW12
   elim (IHT1 … HUT1) -T1 #U #HUT #HU1
   elim (tps_inv_lift1_le … HT2 … HUT ?) -T // [3: /2 width=5/ |2: skip ] #U2 #HU2 #HUT2
-  @ex2_1_intro  [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *)
+  @ex2_intro  [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *)
 | #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #X #d #e #HX
   elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
@@ -85,7 +85,7 @@ lemma tpr_inv_lift1: t_deliftable_sn tpr.
   elim (IHW12 … HW01) -W1 #W3 #HW32 #HW03
   elim (IHT12 … HT01) -T1 #T3 #HT32 #HT03
   elim (lift_trans_le … HV32 … HV2 ?) -V2 // #V2 #HV32 #HV2
-  @ex2_1_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
+  @ex2_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
 | #V #T1 #T #T2 #_ #HT2 #IHT1 #X #d #e #HX
   elim (lift_inv_bind2 … HX) -HX #V3 #T3 #_ #HT31 #H destruct
   elim (IHT1 … HT31) -T1 #T1 #HT1 #HT31
@@ -98,21 +98,24 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-fact tpr_inv_abst1_aux: ∀U1,U2. U1 ➡ U2 → ∀a,V1,T1. U1 = ⓛ{a}V1. T1 →
-                        ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛ{a}V2. T2.
-#U1 #U2 * -U1 -U2
-[ #I #a #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #a #V #T #H destruct
-| #b #V1 #V2 #W #T1 #T2 #_ #_ #a #V #T #H destruct
-| #b #I #V1 #V2 #T1 #T #T2 #HV12 #HT1 #HT2 #a #V0 #T0 #H destruct
-  <(tps_inv_refl_SO2 … HT2 ? ? ?) -T2 /2 width=5/
-| #b #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #a #V0 #T0 #H destruct
-| #V #T1 #T #T2 #_ #_ #a #V0 #T0 #H destruct
-| #V #T1 #T2 #_ #a #V0 #T0 #H destruct
-]
-qed.
-
 (* Basic_1: was pr0_gen_abst *)
 lemma tpr_inv_abst1: ∀a,V1,T1,U2. ⓛ{a}V1. T1 ➡ U2 →
                      ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛ{a}V2. T2.
-/2 width=3/ qed-.
+#a #V1 #T1 #U2 #H elim (tpr_inv_bind1 … H) -H *
+[ #V2 #T #T2 #HV12 #HT1 #HT2
+  lapply (tps_inv_refl_SO2 … HT2 ???) -HT2 // /2 width=5/
+| #T2 #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma tpr_fwd_abst1: ∀a,V1,T1,U2. ⓛ{a}V1.T1 ➡ U2 → ∀b,I,W.
+                     ∃∃V2,T2. ⓑ{b,I}W.T1 ➡ ⓑ{b,I}W.T2 &
+                              U2 = ⓛ{a}V2.T2.
+#a #V1 #T1 #U2 #H #b #I #W elim (tpr_inv_bind1 … H) -H *
+[ #V2 #T #T2 #HV12 #HT1 #HT2
+  lapply (tps_inv_refl_SO2 … HT2 ???) -HT2 // /3 width=4/
+| #T2 #_ #_ #_ #H destruct
+]
+qed-.