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

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma
index 51126ebd102247cf3cae9015ac84fd8bf7512601..acc34d75c987e5a8ee3b547d8bf90c6d777cd678 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma
@@ -41,43 +41,29 @@ qed-.
 (* Basic properties *********************************************************)
 
 lemma fsups_refl: tri_reflexive … fsups.
-/2 width=1/ qed.
+/2 width=1 by tri_inj/ qed.
 
 lemma fsupq_fsups: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
-/2 width=1/ qed.
+/2 width=1 by tri_inj/ qed.
 
 lemma fsups_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
                     ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
-/2 width=5/ qed.
+/2 width=5 by tri_step/ qed.
 
 lemma fsups_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ →
                     ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
-/2 width=5/ qed.
+/2 width=5 by tri_TC_strap/ qed.
+
+lemma fsups_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ →
+                   ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
+                   ⦃G1, L1, U1⦄ ⊃* ⦃G2, K2, T2⦄.
+#G1 #G2 #K1 #K2 #T1 #T2 #H @(fsups_ind … H) -G2 -K2 -T2
+/3 width=5 by fsups_strap1, fsupq_fsups, fsupq_drop/
+qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma fsups_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 //
-/3 width=3 by fsupq_fwd_fw, transitive_le/ (**) (* slow even with trace *)
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2
+/3 width=3 by fsupq_fwd_fw, transitive_le/
 qed-.
-(*
-(* Advanced inversion lemmas on plus-iterated supclosure ********************)
-
-lamma fsupp_inv_bind1_fsups: ∀b,J,G1,G2,L1,L2,W,U,T2. ⦃G1, L1, ⓑ{b,J}W.U⦄ ⊃+ ⦃G2, L2, T2⦄ →
-                             ⦃G1, L1, W⦄ ⊃* ⦃G2, L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⊃* ⦃G2, L2, T2⦄.
-#b #J #G1 #G2 #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H
-  elim (fsup_inv_bind1 … H) -H * #H1 #H2 #H3 destruct /2 width=1/
-| #G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=4/
-]
-qad-.
-
-lamma fsupp_inv_flat1_fsups: ∀J,G1,G2,L1,L2,W,U,T2. ⦃G1, L1, ⓕ{J}W.U⦄ ⊃+ ⦃G2, L2, T2⦄ →
-                             ⦃G1, L1, W⦄ ⊃* ⦃G2, L2, T2⦄ ∨ ⦃G1, L1, U⦄ ⊃* ⦃G2, L2, T2⦄.
-#J #G1 #G2 #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H
-  elim (fsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/
-| #G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=4/
-]
-qad-.
-*)