From c5828dcf6cf9317ffff5bf14d0a65dae7169cd7b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Jun 2014 11:53:04 -0700
Subject: [PATCH] feat(library/standard): add function extensionality axiom

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/standard/funext.lean | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 library/standard/funext.lean

diff --git a/library/standard/funext.lean b/library/standard/funext.lean
new file mode 100644
index 000000000..aa50eebfe
--- /dev/null
+++ b/library/standard/funext.lean
@@ -0,0 +1,7 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+import logic
+
+-- Function extensionality
+axiom funext : ∀ {A : Type} {B : A → Type} {f g : Π x, B x} (H : ∀ x, f x = g x), f = g