update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc
index cc8863b593c6802e18e1405b24b8d39a58fb3a45..8827703c5f62b3c7daed862894aa89a697cd6323 100644 (file)
--- 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.