proposition: Lemma seq_eqv_l A (r : relation A) dom : ⦗dom⦘ ⨾ r ≡ (fun x y => dom x /\ r x y).
proof: Proof. autounfold with unfolderDb; intuition; desf; eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets