X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fetc%2Frelocation%2Fpstream.etc;h=8827703c5f62b3c7daed862894aa89a697cd6323;hb=3c78efa39d4783f83638b1aabe8d776d83aabf35;hp=cc8863b593c6802e18e1405b24b8d39a58fb3a45;hpb=9709aaeb059e24359d5d8a3997ef22974bff3718;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc
index cc8863b59..8827703c5 100644
--- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc
+++ b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc
@@ -18,24 +18,6 @@ include "ground/arith/pnat.ma".
 
 (* RELOCATION P-STREAM ******************************************************)
 
-definition gr_push: gr_map → gr_map ≝ λf. 𝟏⨮f.
-
-interpretation "push (pstream)" 'UpSpoon f = (gr_push f).
-
-definition gr_next: gr_map → gr_map.
-* #p #f @(↑p⨮f)
-defined.
-
-interpretation "next (pstream)" 'UpArrow f = (gr_next f).
-
-(* Basic properties *********************************************************)
-
-lemma gr_push_unfold: ∀f. 𝟏⨮f = ⫯f.
-// qed.
-
-lemma gr_next_unfold: ∀f,p. (↑p)⨮f = ↑(p⨮f).
-// qed.
-
 (* Basic inversion lemmas ***************************************************)
 
 lemma eq_inv_gr_push_bi: injective ? ? gr_push.