proposition: Lemma collect_rel_irr f r (Irr : irreflexive (f ↑ r)): irreflexive r.
proof: Proof. u. eapply Irr. eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets