(* Constructions with pr_uni ************************************************)
(*** fcla_uni *)
-lemma pr_fcla_uni (n): ð\9d\90\82â\9dªð\9d\90®â\9d¨nâ\9d©â\9d« ≘ n.
+lemma pr_fcla_uni (n): ð\9d\90\82â\9d¨ð\9d\90®â\9d¨nâ\9d©â\9d© ≘ n.
#n @(nat_ind_succ … n) -n
/2 width=1 by pr_fcla_isi, pr_fcla_next/
qed.