X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_new%2Fdrops%2Fdrops.etc;h=795f620cdea1350c3649feae6b53e2ad57da46a6;hb=9b8d36ee041582f876543086e7659ed9e365e861;hp=7e53292ef367ade7fc157146a8f8a6fe82f38e85;hpb=952ec5aa2e9a54787acb63a5c8d6fdbf9011ab60;p=helm.git

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 7e53292ef..795f620cd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc
@@ -1,12 +1,3 @@
-lemma drop_refl_atom_O2: ∀s,l. ⬇[s, l, O] ⋆ ≡ ⋆.
-/2 width=1 by drop_atom/ qed.
-
-(* Basic_1: was by definition: drop_refl *)
-lemma drop_refl: ∀L,l,s. ⬇[s, l, 0] L ≡ L.
-#L elim L -L //
-#L #I #V #IHL #l #s @(nat_ind_plus … l) -l /2 width=1 by drop_pair, drop_skip/
-qed.
-
 lemma drop_split: ∀L1,L2,l,m2,s. ⬇[s, l, m2] L1 ≡ L2 → ∀m1. m1 ≤ m2 →
                   ∃∃L. ⬇[s, l, m2 - m1] L1 ≡ L & ⬇[s, l, m1] L ≡ L2.
 #L1 #L2 #l #m2 #s #H elim H -L1 -L2 -l -m2
@@ -32,20 +23,22 @@ 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,t. ⬇*[t] L1 ≡ L2 → ∀t1,t2. t1 ⊚ t2 ≡ t →
-                         ∃∃L. ⬇*[t1] L1 ≡ L & ⬇*[t2] L ≡ L2.
-#L1 #L2 #t #H elim H -L1 -L2 -t
-[ #t1 #t2 #H elim (after_inv_empty3 … H) -H
-  /2 width=3 by ex2_intro, drops_atom/
-| #I #L1 #L2 #V #t #HL12 #IHL12 #t1 #t2 #H elim (after_inv_false3 … H) -H *
-  [ #tl1 #tl2 #H1 #H2 #Ht destruct elim (IHL12 … Ht) -t
-    #tl #H1 #H2
-  | #tl1 #H #Ht destruct elim (IHL12 … Ht) -t
+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 #t #_ #HV21 #IHL12 #t1 #t2 #H elim (after_inv_true3 … H) -H
-  #tl1 #tl2 #H1 #H2 #Ht destruct elim (lifts_split_trans … HV21 … Ht) -HV21
-  elim (IHL12 … Ht) -t /3 width=5 by ex2_intro, drops_skip/
+| #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-.