basic_2: stronger supclosure allows better inversion lemmas

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index dba35a74a47133e5e02215421dc13a2d6cc3f44d..5c3a07a2a0de2eb1b741a642947d8231beb1be88 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -72,10 +72,6 @@ lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
 #R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/
 qed-.
 
-lemma pippo: ∀R1,R2,RP1,RP2. R_confluent_lfxs R1 R2 RP1 RP2 →
-             lexs_confluent R1 R2 RP1 cfull RP2 cfull.
-#R1 #R2 #RP1 #RP2 #HR #f #L0 #T0 #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2 #HL02  
-
 (* Basic inversion lemmas ***************************************************)
 
 lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆.