proposition: Fact sandwich_equiv : star R === star S.
proof: Proof. Proof using H1 H2. split. - apply star_mono, H1. - intros x y H3. apply star_idem. revert x y H3. apply star_mono, H2. Qed.
imports: Morphisms FinFun Undecidability.HOU(std.tactics std.misc std.ars.basic)