proposition: Lemma delift_restr_classes rel : rel_delift eqv (restr_rel (rel_classes eqv) rel) ≡ rel_delift eqv rel.
proof: Proof. Proof using. u; intuition; desf; splits; ins; eauto. Qed.
imports: HahnBase HahnSets HahnRelationsBasic Setoid HahnEquational