proposition: Lemma restr_seq_eqv_l A (f : A -> Prop) d r : restr_rel f (⦗d⦘ ⨾ r) ≡ ⦗d⦘ ⨾ restr_rel f r.
proof: Proof. u; eauto 6. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets