proposition: Fact red_fun_fp_it x n : Normal R x -> it n rho x = x.
proof: Proof. Proof using red. intros H. induction n as [|n IH]; cbn. - reflexivity. - rewrite IH. apply red_fun_fp, H. Qed.
imports: Morphisms FinFun ConstructiveEpsilon Undecidability.HOU(std.tactics std.decidable std.misc std.ars.basic std.ars.confluence)