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