proposition: Lemma mlarge_unshift alpha s : ~In 0 s -> mlarge alpha s <-> mlargeS alpha (unshift s).
proof: Proof. unfold mlarge, mlargeS; intros; rewrite path_to_path_toS_iff; auto; now split. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)