proposition: Lemma restr_set_inter A (s s' : A -> Prop) r : restr_rel (s ∩₁ s') r ≡ restr_rel s r ∩ restr_rel s' r.
proof: Proof. u. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets