proposition: Lemma same_relation_exp A (r r' : relation A) (EQ: r ≡ r') : forall x y, r x y <-> r' x y.
proof: Proof. split; apply EQ. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets