proposition: Fact E_correct x y : evaluates R x y <-> exists n, E n x = Some y.
proof: Proof. Proof using red. split. - intros H. generalize H. intros [n <-] % red. exists (S n). apply E_it, H. - intros [n H]; revert x H. induction n as [|n IH]; cbn; intros x. + discriminate. + destruct (delta x) as [H|H]; intros H1. * assert (x=y) as <- by congruence. split; auto. * apply IH in H1 as [H1 H2]. split; [|exact H2]. rewrite <- H1. apply red. Qed.
imports: Morphisms FinFun ConstructiveEpsilon Undecidability.HOU(std.tactics std.decidable std.misc std.ars.basic std.ars.confluence)