]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / prototerm_constructors_eq.ma
index 88f567214877cd7c3566f502dc1a29bb2897e24a..46e945ede9ed9b0e022b9573cbc96c3d677a7162 100644 (file)
@@ -20,6 +20,6 @@ include "ground/lib/subset_ext_equivalence.ma".
 (* Constructions with equivalence for prototerm *****************************)
 
 lemma iref_eq_repl (t1) (t2) (n):
-      t1 â\87\94 t2 â\86\92 ð\9d\9b\97n.t1 â\87\94 ð\9d\9b\97n.t2.
+      t1 â\87\94 t2 â\86\92 ð\9d\9b\95n.t1 â\87\94 ð\9d\9b\95n.t2.
 /2 width=1 by subset_equivalence_ext_f1_bi/
 qed.