X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpreterm_constructors.ma;h=852fa0a59f204028bec097b7d212fbb0c51e8568;hb=f83215ca9b8d0019c85a991ec90c6c658c0aaff8;hp=003b8d1ce8ed74e479393a001c15145d578fb3cc;hpb=e8571cfbc30a3da656cff0c0e0f0ee747e8c4cdd;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
index 003b8d1ce..852fa0a59 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
@@ -51,7 +51,7 @@ interpretation
 
 lemma preterm_in_root_inv_lcons_oref:
       ∀p,l,n. l◗p ϵ ▵#n →
-      ∧∧ 𝗱❨n❩ = l & 𝐞 = p.
+      ∧∧ 𝗱n = l & 𝐞 = p.
 #p #l #n * #q
 <list_append_lcons_sn #H0 destruct -H0
 elim (eq_inv_list_empty_append … e0) -e0 #H0 #_
@@ -60,7 +60,7 @@ qed-.
 
 lemma preterm_in_root_inv_lcons_iref:
       ∀t,p,l,n. l◗p ϵ ▵𝛗n.t →
-      ∧∧ 𝗱❨n❩ = l & p ϵ ▵t.
+      ∧∧ 𝗱n = l & p ϵ ▵t.
 #t #p #l #n * #q
 <list_append_lcons_sn * #r #Hr #H0 destruct
 /3 width=2 by ex_intro, conj/