update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_after_pat.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat.ma
index 525658c99588e0ecc13fe7545538071f230fc295..c64136a653378cdafeebb563aac0ae321416ce61 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat.ma
@@ -21,8 +21,8 @@ include "ground/relocation/pr_after.ma".
 
 (*** after_at_fwd *)
 lemma pr_after_pat_des (i) (i1):
-      â\88\80f. @â\9dªi1, fâ\9d« ≘ i → ∀f2,f1. f2 ⊚ f1 ≘ f →
-      â\88\83â\88\83i2. @â\9dªi1, f1â\9d« â\89\98 i2 & @â\9dªi2, f2â\9d« ≘ i.
+      â\88\80f. @â\9d¨i1, fâ\9d© ≘ i → ∀f2,f1. f2 ⊚ f1 ≘ f →
+      â\88\83â\88\83i2. @â\9d¨i1, f1â\9d© â\89\98 i2 & @â\9d¨i2, f2â\9d© ≘ i.
 #i elim i -i [2: #i #IH ] #i1 #f #Hf #f2 #f1 #Hf21
 [ elim (pr_pat_inv_succ_dx … Hf) -Hf [1,3:* |*: // ]
   [1: #g #j1 #Hg #H0 #H |2,4: #g #Hg #H ]
@@ -40,8 +40,8 @@ qed-.
 
 (*** after_fwd_at *)
 lemma pr_after_des_pat (i) (i2) (i1):
-      â\88\80f1,f2. @â\9dªi1, f1â\9d« â\89\98 i2 â\86\92 @â\9dªi2, f2â\9d« ≘ i →
-      â\88\80f. f2 â\8a\9a f1 â\89\98 f â\86\92 @â\9dªi1, fâ\9d« ≘ i.
+      â\88\80f1,f2. @â\9d¨i1, f1â\9d© â\89\98 i2 â\86\92 @â\9d¨i2, f2â\9d© ≘ i →
+      â\88\80f. f2 â\8a\9a f1 â\89\98 f â\86\92 @â\9d¨i1, fâ\9d© ≘ i.
 #i elim i -i [2: #i #IH ] #i2 #i1 #f1 #f2 #Hf1 #Hf2 #f #Hf
 [ elim (pr_pat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
   #g2 [ #j2 ] #Hg2 [ #H22 ] #H20
@@ -60,16 +60,16 @@ qed-.
 
 (*** after_fwd_at2 *)
 lemma pr_after_des_pat_sn (i1) (i):
-      â\88\80f. @â\9dªi1, fâ\9d« â\89\98 i â\86\92 â\88\80f1,i2. @â\9dªi1, f1â\9d« ≘ i2 →
-      â\88\80f2. f2 â\8a\9a f1 â\89\98 f â\86\92 @â\9dªi2, f2â\9d« ≘ i.
+      â\88\80f. @â\9d¨i1, fâ\9d© â\89\98 i â\86\92 â\88\80f1,i2. @â\9d¨i1, f1â\9d© ≘ i2 →
+      â\88\80f2. f2 â\8a\9a f1 â\89\98 f â\86\92 @â\9d¨i2, f2â\9d© ≘ i.
 #i1 #i #f #Hf #f1 #i2 #Hf1 #f2 #H elim (pr_after_pat_des … Hf … H) -f
 #j1 #H #Hf2 <(pr_pat_mono … Hf1 … H) -i1 -i2 //
 qed-.
 
 (*** after_fwd_at1 *)
 lemma pr_after_des_pat_dx (i) (i2) (i1):
-      â\88\80f,f2. @â\9dªi1, fâ\9d« â\89\98 i â\86\92 @â\9dªi2, f2â\9d« ≘ i →
-      â\88\80f1. f2 â\8a\9a f1 â\89\98 f â\86\92 @â\9dªi1, f1â\9d« ≘ i2.
+      â\88\80f,f2. @â\9d¨i1, fâ\9d© â\89\98 i â\86\92 @â\9d¨i2, f2â\9d© ≘ i →
+      â\88\80f1. f2 â\8a\9a f1 â\89\98 f â\86\92 @â\9d¨i1, f1â\9d© ≘ i2.
 #i elim i -i [2: #i #IH ] #i2 #i1 #f #f2 #Hf #Hf2 #f1 #Hf1
 [ elim (pr_pat_inv_succ_dx … Hf) -Hf [1,3: * |*: // ]
   #g [ #j1 ] #Hg [ #H01 ] #H00