proposition: Fact tak_cofinal x y : x >* y -> exists n, y >* it n rho x.
proof: Proof. Proof using tak. induction 1 as [x |x x' y H _ (n&IH)]. - exists 0. cbn. constructor. - exists (S n). rewrite IH. cbn. apply star_exp. apply tak, tak_mono_n, H. Qed.
imports: Morphisms FinFun Undecidability.HOU(std.tactics std.misc std.ars.basic)