Still a problem to be fixed: after reaching the border we must always add

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / fsupq_alt.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma
index 54e161f7f4dc165115880e2f81f613ea493ae739..cfbca86937fb020f5cb0d8bce3347181dd1b8982 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma
@@ -29,20 +29,18 @@ interpretation
 lemma fsupqa_refl: tri_reflexive … fsupqa.
 // qed.
 
-lemma fsupqa_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃⊃⸮ ⦃G2, K2, T2⦄ →
-                    ∀L1,d,e. ⇩[d, e] L1 ≡ K1 →
-                    ∀U1. ⇧[d, e] T1 ≡ U1 → ⦃G1, L1, U1⦄ ⊃⊃⸮ ⦃G2, K2, T2⦄.
-#G1 #G2 #K1 #K2 #T1 #T2 * [ /3 width=7/ ] * #H1 #H2 #H3 destruct
-#L1 #d #e #HLK #U1 #HTU elim (eq_or_gt e)
-/3 width=5 by fsup_ldrop_lt, or_introl/ #H destruct
->(ldrop_inv_O2 … HLK) -L1 >(lift_inv_O2 … HTU) -T2 -d //
+lemma fsupqa_drop: ∀G,L,K,T,U,e.
+                   ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄.
+#G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e)
+/3 width=5 by fsup_drop_lt, or_introl/ #H destruct
+>(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T //
 qed.
 
 (* Main properties **********************************************************)
 
 theorem fsupq_fsupqa: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄.
 #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/2 width=7 by fsupqa_ldrop, fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, or_introl/
+/2 width=3 by fsupqa_drop, fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, or_introl/
 qed.
 
 (* Main inversion properties ************************************************)