diff --git a/encodings/bool_hol.lp b/encodings/bool_hol.lp
index 338788c0d99d697a481a8fb69796b78b70d415f7..97c88564ad27504d87962bb35c3bdd40d290d29a 100644
--- a/encodings/bool_hol.lp
+++ b/encodings/bool_hol.lp
@@ -31,3 +31,5 @@ set infix 2 "=" ≔ eq
 set builtin "eq" ≔ eq // FIXME emacs indentation
 
 rule ε ($x = $y) ↪ Πp: η (_ ~> bool), ε (p $x) → ε (p $y)
+
+definition iff P Q ≔ (P ⊃ (λ_, Q)) ∧ ((λ_, Q ⊃ (λ_, P)))
diff --git a/encodings/builtins.lp b/encodings/builtins.lp
index 79d9368f3c7dca8d40e4d71d17d05d130e87859d..ef313a8479ffa85ceef5e13dfb71544e7f0aa2c2 100644
--- a/encodings/builtins.lp
+++ b/encodings/builtins.lp
@@ -23,3 +23,6 @@ constant symbol str_cons: η {|!Number!|} → η {|!String!|} → η {|!String!|
 
 set declared "∃"
 definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (∀ (λx, ¬ (P x)))
+
+symbol propositional_extensionality:
+  ε (∀ {bool} (λp, (∀ {bool} (λq, (iff p q) ⊃ (λ_, eq {bool} p q)))))
diff --git a/prelude/functions.lp b/prelude/functions.lp
index ebfd9f6a1696c7b601084bf27be7d337ab4e6f69..efdf9dd8cd482387eb6aed582f24cbc647dd94a2 100644
--- a/prelude/functions.lp
+++ b/prelude/functions.lp
@@ -7,9 +7,10 @@ require open personoj.prelude.logic
 // functions [D, R: TYPE]
 //
 
-// symbol
-// extensionality_postulate (D R: Term uType) (f g: Term (D ~> R))
-// : Term (biff (forall (λx: Term D, f x = g ) (f = g)))
+symbol extensionality_postulate:
+  ε (∀B (λD, ∀B (λR,
+                 ∀ (λf: η (D ~> R),
+                    ∀ (λg: η (D ~> R), iff (∀ (λx, f x = g x)) (f = g))))))
 
 // definition {|injective?|} {D} {R} (f: Term (D ~> R)) ≔
 //   forall (λx1, forall (λx2, imp (f x1 = f x2) (x1 = x2)))