(* 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.