X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fetc%2Frelocation%2Ftr.etc;h=a0aba6e512d84bafbcfc0d3af918d9bcfd0f77f3;hb=ad49f5895fadff5a1d9845debb1c852a1455c6c9;hp=ba3287eb6d5193fc1b579433f54d58854fde1f61;hpb=ca1807b86671236be3042b77dbc65034d0aa77c2;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc
index ba3287eb6..a0aba6e51 100644
--- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc
+++ b/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc
@@ -3,14 +3,6 @@ lemma pippo (f):
 * #p #f //
 qed.
 
-corec lemma tr_compose_id_dx (f):
-            f ≗ f∘𝐢.
-cases tr_id_unfold
-cases tr_compose_unfold
-cases (pippo f) in ⊢ (??%?);
-@stream_eq_cons /2 width=1 by/
-qed.
-
 axiom pippo2 (f) (p):
       f@❨p❩ + (⇂*[ninj p]f)@❨𝟏❩ = f@❨↑p❩.