Proving that inclusion is antisymmetric in Coq 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 -&gt; set -&gt; Prop.
Definition subset (x:set) (y:set) := forall z:set, element z x -&gt; element z y.
Axiom equality : forall x y:set, x = y &lt;-&gt; forall z:set, element z x &lt;-&gt; element z y.
Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -&gt; x = y.
Proof.
intros a b.
unfold subset.
intro H.
destruct H as [H0 H1].


At this point I get the following output:

1 subgoal
set : Type
element : set -&gt; set -&gt; Prop
a : set
b : set
H0 : forall z : set, element z a -&gt; element z b
H1 : forall z : set, element z b -&gt; element z a
______________________________________(1/1)
a = b


I'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.
Theorem inclusion_is_antisymmetric : forall x y:set, subset x y /\ subset y x -&gt; x = y.
Proof.
  firstorder using equality.
Qed.