proposition: Theorem TMT rho : Reflexive S -> tak_fun S rho -> confluent R.
proof: Proof. Proof using H1 H2. intros H3 H4. eapply sandwich_confluent, tak_diamond, H4. Qed.
imports: Morphisms FinFun Undecidability.HOU(std.tactics std.misc std.ars.basic)