proposition: Lemma call_lt_wf : well_founded call_lt.
proof: Proof. unfold call_lt; apply Inverse_Image.wf_inverse_image, wf_lexico. - apply E0lt_wf. - unfold Peano.lt; apply Nat.lt_wf_0. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)