X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_after_ist_isi.ma;h=16d2ebc8d85a4d87faae455ca6dde671d761bcde;hb=b1c5b3370653db6e495bbf6b3799cba592746cdd;hp=ea312f5a018fb569a5e3b59b8892f94a6ee566e0;hpb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma
index ea312f5a0..16d2ebc8d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_after_ist.ma".
 
 (*** after_fwd_isid_sn *)
 lemma pr_after_des_ist_eq_sn:
-      ∀f2,f1,f. 𝐓❪f❫ → f2 ⊚ f1 ≘ f → f1 ≡ f → 𝐈❪f2❫.
+      ∀f2,f1,f. 𝐓❨f❩ → f2 ⊚ f1 ≘ f → f1 ≐ f → 𝐈❨f2❩.
 #f2 #f1 #f #H #Hf elim (pr_after_inv_ist … Hf H) -H
 #Hf2 #Hf1 #H @pr_isi_pat_total // -Hf2
 #i2 #i #Hf2 elim (Hf1 i2) -Hf1
@@ -32,7 +32,7 @@ qed-.
 
 (*** after_fwd_isid_dx *)
 lemma pr_after_des_ist_eq_dx:
-      ∀f2,f1,f.  𝐓❪f❫ → f2 ⊚ f1 ≘ f → f2 ≡ f → 𝐈❪f1❫.
+      ∀f2,f1,f.  𝐓❨f❩ → f2 ⊚ f1 ≘ f → f2 ≐ f → 𝐈❨f1❩.
 #f2 #f1 #f #H #Hf elim (pr_after_inv_ist … Hf H) -H
 #Hf2 #Hf1 #H2 @pr_isi_pat_total // -Hf1
 #i1 #i2 #Hi12 elim (pr_after_des_ist_pat … Hi12 … Hf) -f1