proposition: Fact E_stops n x: Normal R x -> E (S n) x = Some x.
proof: Proof. cbn; destruct delta; intuition. Qed.
imports: Morphisms FinFun ConstructiveEpsilon Undecidability.HOU(std.tactics std.decidable std.misc std.ars.basic std.ars.confluence)