proposition: Lemma delift_lift rel : rel_delift eqv (rel_lift eqv rel) ≡ eqv ⨾ rel ⨾ eqv.
proof: Proof. Proof using SYM TRAN. u; splits; ins; desf; splits; ins; desf; eauto 8. do 2 eexists; splits; eauto. Qed.
imports: HahnBase HahnSets HahnRelationsBasic Setoid HahnEquational