proposition: Remark f_ok_inv : forall k, mlarge (T1.phi0 alpha) (interval (S k) (Nat.pred (f (S k)))).
proof: Proof. inversion_clear f_ok; assumption. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)