proposition: Fact E_step n x y: E n x = Some y -> E (S n) x = Some y.
proof: Proof. induction n in x, y |-*; cbn; try discriminate. destruct (delta x); eauto. Qed.
imports: Morphisms FinFun ConstructiveEpsilon Undecidability.HOU(std.tactics std.decidable std.misc std.ars.basic std.ars.confluence)