proposition: Lemma same_relation_restr A (f : A -> Prop) r r' : (forall x (CONDx: f x) y (CONDy: f y), r x y <-> r' x y) -> (restr_rel f r ≡ restr_rel f r').
proof: Proof. u; firstorder. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets