- updated equivalence on referred entries: it nust be degree-based

[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
deleted file mode 100644 (file)
index 906c85c..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc
+++ /dev/null
@@ -1,13 +0,0 @@
-(* Inversion lemmas on equivalence ******************************************)
-
-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-.