proposition: Lemma collect_rel_acyclic f r (ACYC : acyclic (f ↑ r)): acyclic r.
proof: Proof. unfold acyclic in *. eapply collect_rel_irr. eby erewrite collect_rel_ct. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets