proposition: Lemma L_spec_compat alpha (f g : nat -> nat) : L_spec alpha f -> (forall n, f n = g n) -> L_spec alpha g.
proof: Proof. destruct 1. - left; congruence. - right; [trivial | intros ; rewrite <- H1; auto]. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)