proposition: Lemma restr_set_union A (s s' : A -> Prop) r : restr_rel (s ∪₁ s') r ≡ restr_rel s r ∪ restr_rel s' r ∪ ⦗s⦘ ⨾ r ⨾ ⦗s'⦘ ∪ ⦗s'⦘ ⨾ r ⨾ ⦗s⦘.
proof: Proof. u; eauto 10. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets