proposition: Lemma exercise1_1: (x=y) <-> (forall X, inc x X -> inc y X).
proof: Proof. split; first by move=> ->. move=> spec_sub; symmetry; apply: set1_eq; apply: spec_sub; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)