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