proposition: Fact diamond_ext R S: R === S -> diamond S -> diamond R.
proof: Proof. intros H1 H2 x y z H3 H4. assert (joinable S y z); firstorder. Qed.
imports: Morphisms FinFun Undecidability.HOU(std.tactics std.misc std.ars.basic)