proposition: Lemma crs_cross (s s' : A -> Prop) : (s × s')^⋈? ≡ ⦗fun _ => True⦘ ∪ s × s' ∪ s' × s.
proof: Proof. rewrite !crsE. u. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets