matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc

   1 lemma pippo: ∀L1,L2,t1. ⬇*[Ⓕ, t1] L1 ≡ L2 → ∀t2. ⬇*[Ⓕ, t2] L1 ≡ L2 →
   2 |t1| + ∥t2∥ = ∥t1∥ + |t2|.
   3 #L1 #L2 #t1 #H elim H -L1 -L2 -t1
   4 [ #t1 #Ht1 #t2 #H elim (drops_inv_atom1 … H) -H
   5   #_ #Ht2 >Ht1 -Ht1 // >Ht2 -Ht2 //
   6 | #I #L1 #L2 #V #t1 #_ #IH #t2 #H normalize
   7
   8 lemma drop_conf_div: ∀I1,L,K,V1,m1. ⬇[m1] L ≡ K.ⓑ{I1}V1 →
   9                      ∀I2,V2,m2. ⬇[m2] L ≡ K.ⓑ{I2}V2 →
  10                      ∧∧ m1 = m2 & I1 = I2 & V1 = V2.
  11 #I1 #L #K #V1 #m1 #HLK1 #I2 #V2 #m2 #HLK2
  12 elim (yle_split m1 m2) #H
  13 elim (yle_inv_plus_sn … H) -H #m #Hm
  14 [ lapply (drop_conf_ge … HLK1 … HLK2 … Hm ?)
  15 | lapply (drop_conf_ge … HLK2 … HLK1 … Hm ?)
  16 ] -HLK1 -HLK2 // #HK
  17 lapply (drop_fwd_length … HK) #H
  18 elim (discr_yplus_x_xy … H) -H
  19 [1,3: #H elim (ylt_yle_false (|K.ⓑ{I1}V1|) (∞)) // ]
  20 #H destruct
  21 lapply (drop_inv_O2 … HK) -HK #H destruct
  22 /2 width=1 by and3_intro/
  23 qed-.