proposition: Lemma map_rel_acyclic f r (ACYC : acyclic r): acyclic (f ↓ r).
proof: Proof. unfold acyclic in *. erewrite map_rel_ct. by eapply map_rel_irr. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets