proposition: Lemma irreflexive_bunion (s : B -> Prop) (rr : B -> relation A) : irreflexive (bunion s rr) <-> forall x, s x -> irreflexive (rr x).
proof: Proof. unfold irreflexive, bunion; repeat split; try red; ins; desf; eauto. Qed.
imports: HahnBase HahnList Relations