proposition: Lemma exercise1_2: exists x y:Set, x <> y.
proof: Proof. have theorem:forall x, emptyset <> singleton x. by move=> x esx; empty_tac1 x. by exists emptyset; exists (singleton emptyset); apply: theorem. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)