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