extensionality

czf.v

@@ -184,6 +184,12 @@ Proof.
   rewrite <- Ha. rewrite <- Hb. apply Hs.
 Qed.
 
+Instance subseteq_reflexive : Reflexive (subseteq : relation V).
+Proof. intros ?. unfold subseteq, subseteq_V. auto. Qed.
+
+Instance subseteq_transitive : Transitive (subseteq : relation V).
+Proof. intros ???. unfold subseteq, subseteq_V. auto. Qed.
+
 Lemma V_ext (a b : V) :
   a ⊆ b → b ⊆ a → a ≡ b.
 Proof.
@@ -200,7 +206,13 @@ Qed.
 (** * Axioms *)
 
 (** Extensionality *)
-(* ... *)
+Theorem CZF_extensionality (a b : V) :
+  a ⊆ b ∧ b ⊆ a ↔ a ≡ b.
+Proof.
+  split.
+  - intros [? ?]. apply V_ext; auto.
+  - intros ->. split; auto.
+Qed.
 
 (** Paring *)
 Lemma CZF_pairing (x y : V) :