update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / etc / relocation / tr.etc

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc
index ba3287eb6d5193fc1b579433f54d58854fde1f61..a0aba6e512d84bafbcfc0d3af918d9bcfd0f77f3 100644 (file)
--- 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.
 
 * #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❩.
 
 axiom pippo2 (f) (p):
       f@❨p❩ + (⇂*[ninj p]f)@❨𝟏❩ = f@❨↑p❩.