(* 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.
+lemma iref_eq_repl (t1) (t2) (k):
+ t1 â\87\94 t2 â\86\92 ð\9d\9b\95k.t1 â\87\94 ð\9d\9b\95k.t2.
/2 width=1 by subset_equivalence_ext_f1_bi/
qed.