proposition: Fact E_monotone n m x y: n <= m -> E n x = Some y -> E m x = Some y.
proof: Proof. induction 1 in x, y |-*; eauto using E_step. Qed.
imports: Morphisms FinFun ConstructiveEpsilon Undecidability.HOU(std.tactics std.decidable std.misc std.ars.basic std.ars.confluence)