proposition: Lemma restr_of_crs (s : A -> Prop) r : restr_rel s r^⋈? ≡ ⦗s⦘ ∪ restr_rel s r^⋈.
proof: Proof. rewrite !csE, !crsE. u. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets