notational update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / nstream_coafter.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
index c158f25930fe6d454e3b0f6884e7d3b3358b0126..66ba11b18284e3bc6de75181fb03b46a545ccdac 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
@@ -20,7 +20,7 @@ include "ground_2/relocation/rtmap_coafter.ma".
 rec definition fun0 (n1:nat) on n1: rtmap → nat.
 * * [ | #n2 #f2 @0 ]
 #f2 cases n1 -n1 [ @0 ]
-#n1 @(⫯(fun0 n1 f2))
+#n1 @(â\86\91(fun0 n1 f2))
 defined.
 
 rec definition fun2 (n1:nat) on n1: rtmap → rtmap.
@@ -45,15 +45,15 @@ interpretation "functional co-composition (nstream)"
 (* Basic properties on funs *************************************************)
 
 (* Note: we need theese since matita blocks recursive δ when ι is blocked *)  
-lemma fun0_xn: â\88\80f2,n1. 0 = fun0 n1 (⫯f2).
+lemma fun0_xn: â\88\80f2,n1. 0 = fun0 n1 (â\86\91f2).
 * #n2 #f2 * //
 qed.
 
-lemma fun2_xn: â\88\80f2,n1. f2 = fun2 n1 (⫯f2).
+lemma fun2_xn: â\88\80f2,n1. f2 = fun2 n1 (â\86\91f2).
 * #n2 #f2 * //
 qed.
 
-lemma fun1_xxn: â\88\80f2,f1,n1. fun1 n1 f1 (⫯f2) = n1@f1.
+lemma fun1_xxn: â\88\80f2,f1,n1. fun1 n1 f1 (â\86\91f2) = n1@f1.
 * #n2 #f2 #f1 * //
 qed.
 
@@ -65,22 +65,22 @@ qed.
 
 (* Basic inversion lemmas on compose ****************************************)
 
-lemma cocompose_inv_ppx: â\88\80f2,f1,f,x. (â\86\91f2) ~â\88\98 (â\86\91f1) = x@f →
+lemma cocompose_inv_ppx: â\88\80f2,f1,f,x. (⫯f2) ~â\88\98 (⫯f1) = x@f →
                          0 = x ∧ f2 ~∘ f1 = f.
 #f2 #f1 #f #x
 <cocompose_rew #H destruct
 normalize /2 width=1 by conj/
 qed-.
 
-lemma cocompose_inv_pnx: â\88\80f2,f1,f,n1,x. (â\86\91f2) ~â\88\98 ((⫯n1)@f1) = x@f →
-                         â\88\83â\88\83n. ⫯n = x & f2 ~∘ (n1@f1) = n@f.
+lemma cocompose_inv_pnx: â\88\80f2,f1,f,n1,x. (⫯f2) ~â\88\98 ((â\86\91n1)@f1) = x@f →
+                         â\88\83â\88\83n. â\86\91n = x & f2 ~∘ (n1@f1) = n@f.
 #f2 #f1 #f #n1 #x
 <cocompose_rew #H destruct
 @(ex2_intro … (fun0 n1 f2)) // <cocompose_rew
 /3 width=1 by eq_f2/
 qed-.
 
-lemma cocompose_inv_nxx: â\88\80f2,f1,f,n1,x. (⫯f2) ~∘ (n1@f1) = x@f →
+lemma cocompose_inv_nxx: â\88\80f2,f1,f,n1,x. (â\86\91f2) ~∘ (n1@f1) = x@f →
                          0 = x ∧ f2 ~∘ (n1@f1) = f.
 #f2 #f1 #f #n1 #x
 <cocompose_rew #H destruct