advances in the theory of drops, lexs, and frees ...

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc
index d7356d0b7f6b9b222f1f48e4091bc1dca06d33cb..906c85c73bca71ead7ba99b4059ac04510d2c411 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc
@@ -1,23 +1,13 @@
-lemma pippo: ∀L1,L2,t1. ⬇*[Ⓕ, t1] L1 ≡ L2 → ∀t2. ⬇*[Ⓕ, t2] L1 ≡ L2 →
-|t1| + ∥t2∥ = ∥t1∥ + |t2|.
-#L1 #L2 #t1 #H elim H -L1 -L2 -t1
-[ #t1 #Ht1 #t2 #H elim (drops_inv_atom1 … H) -H
-  #_ #Ht2 >Ht1 -Ht1 // >Ht2 -Ht2 //
-| #I #L1 #L2 #V #t1 #_ #IH #t2 #H normalize 
+(* Inversion lemmas on equivalence ******************************************)
 
-lemma drop_conf_div: ∀I1,L,K,V1,m1. ⬇[m1] L ≡ K.ⓑ{I1}V1 →
-                     ∀I2,V2,m2. ⬇[m2] L ≡ K.ⓑ{I2}V2 →
-                     ∧∧ m1 = m2 & I1 = I2 & V1 = V2.
-#I1 #L #K #V1 #m1 #HLK1 #I2 #V2 #m2 #HLK2
-elim (yle_split m1 m2) #H
-elim (yle_inv_plus_sn … H) -H #m #Hm
-[ lapply (drop_conf_ge … HLK1 … HLK2 … Hm ?)
-| lapply (drop_conf_ge … HLK2 … HLK1 … Hm ?)
-] -HLK1 -HLK2 // #HK
-lapply (drop_fwd_length … HK) #H
-elim (discr_yplus_x_xy … H) -H
-[1,3: #H elim (ylt_yle_false (|K.ⓑ{I1}V1|) (∞)) // ]
-#H destruct
-lapply (drop_inv_O2 … HK) -HK #H destruct
-/2 width=1 by and3_intro/
+lemma drop_O1_inj: ∀i,L1,L2,K. ⬇[i] L1 ≡ K → ⬇[i] L2 ≡ K → L1 ⩬[i, ∞] L2.
+#i @(ynat_ind … i) -i
+[ #L1 #L2 #K #H <(drop_inv_O2 … H) -K #H <(drop_inv_O2 … H) -L1 //
+| #i #IHi * [2: #L1 #I1 #V1 ] * [2,4: #L2 #I2 #V2 ] #K #HLK1 #HLK2 //
+  lapply (drop_fwd_length … HLK1)
+  <(drop_fwd_length … HLK2) [ /4 width=5 by drop_inv_drop1, lreq_succ/ ]
+  #H [ elim (ysucc_inv_O_sn … H) | elim (ysucc_inv_O_dx … H) ]
+| #L1 #L2 #K #H1 lapply (drop_fwd_Y2 … H1) -H1
+  #H elim (ylt_yle_false … H) //
+]
 qed-.