proposition: Lemma confluence_step: confluent (@step X).
proof: Proof. eapply TMT. eapply sandwich_step. eapply sandwich_steps. typeclasses eauto. eapply tak_fun_rho. Qed.
imports: Morphisms Setoid Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms semantics)