proposition: Lemma restr_eq_seq_eqv_r A (r : relation A) B (f : A -> B) dom : restr_eq_rel f (r⨾ ⦗dom⦘) ≡ restr_eq_rel f r⨾ ⦗dom⦘.
proof: Proof. u. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets