diff --git a/demo/kitchen-sink/docs/lean.lean b/demo/kitchen-sink/docs/lean.lean
new file mode 100644
index 00000000..40e82753
--- /dev/null
+++ b/demo/kitchen-sink/docs/lean.lean
@@ -0,0 +1,9 @@
+import logic
+section
+  variables (A : Type) (p q : A → Prop)
+
+  example : (∀x : A, p x ∧ q x) → ∀y : A, p y  :=
+  assume H : ∀x : A, p x ∧ q x,
+  take y : A,
+  show p y, from and.elim_left (H y)
+end