proposition: Lemma exercise1_6: (forall y, y = choose (fun x => (forall z, (inc z x) <-> (inc z y)))) -> (forall a b : Set, sub a b -> sub b a -> a = b).
proof: Proof. move=> hyp a b; rewrite /sub => sab sba. rewrite (hyp a) (hyp b). apply: choose_equiv; move=> x. split; move=> aux z; rewrite aux; split; auto. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)