proposition: Fact E_S n x : E (S n) x = if delta x then Some x else E n (rho x).
proof: Proof. reflexivity. Qed.
imports: Morphisms FinFun ConstructiveEpsilon Undecidability.HOU(std.tactics std.decidable std.misc std.ars.basic std.ars.confluence)