proposition: Lemma seq_eqv_minus_ll A (s : A -> Prop) (r r' : relation A) : (⦗s⦘ ⨾ r) \ r' ≡ ⦗s⦘ ⨾ (r \ r').
proof: Proof. autounfold with unfolderDb; intuition; desf; eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets