proposition: Lemma compute_evaluation_step (s: exp X): (exists t, s ▷ t) -> { t | s ▷ t }.
proof: Proof. intros; eapply compute_evaluation with (S := par) (rho := rho); eauto using tak_fun_rho. all: typeclasses eauto. Qed.
imports: Morphisms Setoid Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order normalisation)