]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / prototerm_proper_constructors.ma
index c7bb79244876fad03c2454df4228db67e2a6e6db..309eb00246b0a93089a18aead73907caf3dab2c4 100644 (file)
@@ -20,6 +20,6 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 (* Constructions with prototerm constructors ********************************)
 
 lemma ppc_iref (t) (n):
-      (ð\9d\9b\97n.t) ϵ 𝐏.
+      (ð\9d\9b\95n.t) ϵ 𝐏.
 #t #n #p * #q #Hq #H0 destruct //
 qed.