update in ground and static_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_lt.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_lt.ma
index 8fc080ed62317516833515d565b5d0fe19467a37..648c27f7197fab9ae455defeb84997d582dbc38c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_lt.ma
@@ -40,7 +40,7 @@ lemma gr_pat_increasing_strict (g) (i1) (i2):
 qed-.
 
 (*** at_fwd_id_ex *)
-lemma gr_pat_des_id (f) (i): @â\9dªi,fâ\9d« â\89\98 i â\86\92 ⫯⫱f = f.
+lemma gr_pat_des_id (f) (i): @â\9dªi,fâ\9d« â\89\98 i â\86\92 ⫯⫰f = f.
 #f elim (gr_map_split_tl f) //
 #H #i #Hf elim (gr_pat_inv_next … Hf … H) -Hf -H
 #j2 #Hg #H destruct lapply (gr_pat_increasing … Hg) -Hg