- new component "s_transition" for the restored fqu and fquq

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc_new / drops / drops.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc
index 795f620cdea1350c3649feae6b53e2ad57da46a6..86ca4c76a43d973aa3ee394c156ed61f4a2f7a26 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc
@@ -22,26 +22,6 @@ lemma drop_split: ∀L1,L2,l,m2,s. ⬇[s, l, m2] L1 ≡ L2 → ∀m1. m1 ≤ m2
 ]
 qed-.
 
-(* Basic_2A1: includes: drop_split *)
-lemma drops_split_trans: ∀L1,L2,f,c. ⬇*[c, f] L1 ≡ L2 → ∀f1,f2. f1 ⊚ f2 ≡ f →
-                         ∃∃L. ⬇*[c, f1] L1 ≡ L & ⬇*[c, f2] L ≡ L2.
-#L1 #L2 #f #c #H elim H -L1 -L2 -f
-[ #f #Hc #f1 #f2 #Hf @(ex2_intro … (⋆)) @drops_atom
-  #H lapply (Hc H) -c
-  #H elim (after_inv_isid3 … Hf H) -f //
-| #I #L1 #L2 #V #f #HL12 #IHL12 #f1 #f2 #Hf elim (after_inv_xxS … Hf) -Hf *
-  [ #g1 #g2 #Hf #H1 #H2 destruct elim (IHL12 … Hf) -f
-    #L #HL1 #HL2 @(ex2_intro … (L.ⓑ{I}V)) /2 width=1 by drops_drop/
-    @drops_skip //
-  | #g1 #Hf #H destruct elim (IHL12 … Hf) -f
-    /3 width=5 by ex2_intro, drops_drop/
-  ]
-| #I #L1 #L2 #V1 #V2 #f #_ #HV21 #IHL12 #f1 #f2 #Hf elim (after_inv_xxO … Hf) -Hf
-  #g1 #g2 #Hf #H1 #H2 destruct elim (lifts_split_trans … HV21 … Hf) -HV21
-  elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip/
-]
-qed-.
-
 lemma drop_inv_refl: ∀L,l,m. ⬇[Ⓕ, l, m] L ≡ L → m = 0.
 /2 width=5 by drop_inv_length_eq/ qed-.