xoa: change in naming convenctions for existential quantifies

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / tps_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma
index 5ffc949222a0323d15344a78b1a83432f14ea5c3..808f6e3ba98f82a9eb1e84db0bdc0e17757e4800 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma
@@ -181,7 +181,7 @@ lemma tps_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 →
     lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
     elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid -Hdie
     #V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O #H
-    @ex2_1_intro [3: @H | skip | @tps_subst [3,5,6: // |1,2: skip | >commutative_plus >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
+    @ex2_intro [3: @H | skip | @tps_subst [3,5,6: // |1,2: skip | >commutative_plus >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
   ]
 | #L #a #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
@@ -214,7 +214,7 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 →
   lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
   elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hdei -Hdie 
   #V0 #HV10 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O #H
-  @ex2_1_intro [3: @H | skip | @tps_subst [5,6: // |1,2: skip | /2 width=1/ | >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
+  @ex2_intro [3: @H | skip | @tps_subst [5,6: // |1,2: skip | /2 width=1/ | >plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *)
 | #L #a #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
   elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
   elim (le_inv_plus_l … Hdetd) #_ #Hedt