I'm a Coq newbie and I'd like to prove that the inclusion relation is antisymmetric, that is: $\forall x\forall y(x\subseteq y\land y\subseteq x\rightarrow x=y)$.I wrote the following thing:Section Test.Variable set : Type.Variable element : set -> set -> Prop.Definition subset (x:set) (y:set) := forall z:set, element z x -> element z y.Axiom equality : forall x y:set, x = y <-> forall z:set, element z x <-> element z y.Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -> x = y.Proof.intros a b.unfold subset.intro H.destruct H as [H0 H1].At this point I get the following output:1 subgoalset : Typeelement : set -> set -> Propa : setb : setH0 : forall z : set, element z a -> element z bH1 : forall z : set, element z b -> element z a______________________________________(1/1)a = bI'm stuck now because I don't know how to:change the goal from $a=b$ to $\forall z(z\in a\leftrightarrow z\in b)$ and then to $c\in a\leftrightarrow c\in b$change H0 from $\forall z(z\in a\rightarrow z\in b)$ to $c\in a\rightarrow c\in b$change H1 from $\forall z(z\in b\rightarrow z\in c)$ to $c\in b\rightarrow c\in a$That is, I know how to prove this theorem on paper but not with Coq.
Proving that inclusion is antisymmetric in Coq
coq;set theory