From a27e73014cd4e72640054532442c1565047cdd66 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Tue, 22 Jan 2019 11:20:15 +0100
Subject: [PATCH] extensionality

---
 czf.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/czf.v b/czf.v
index 7fb2d99..b9438d0 100644
--- a/czf.v
+++ b/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) :