proposition: Fact tak_mono_n x y n : x > y -> it n rho x > it n rho y.
proof: Proof. Proof using tak. intros H. induction n as [|n IH]; cbn. - exact H. - apply tak_mono, IH. Qed.
imports: Morphisms FinFun Undecidability.HOU(std.tactics std.misc std.ars.basic)