proposition: Lemma acyclic_lift : acyclic (rel_lift eqv r) <-> acyclic (r ⨾ eqv).
proof: Proof. Proof using REFL SYM TRAN. unfold acyclic; rewrite ct_lift. unfold rel_lift, irreflexive; split; ins; desc; eauto 6. apply (H x0), ct_end; apply ct_end in H0; u; eauto 10. Qed.
imports: HahnBase HahnSets HahnRelationsBasic Setoid HahnEquational