diff --git a/examples/ex1.lean b/examples/ex1.lean
new file mode 100644
index 0000000000..a2ee83e011
--- /dev/null
+++ b/examples/ex1.lean
@@ -0,0 +1,26 @@
+Variable a : Bool
+Variable b : Bool
+(* Conjunctions *)
+Show a && b
+Show a && b && a
+Show a /\ b
+Show a ∧ b
+Show (and a b)
+Show and a b
+(* Disjunctions *)
+Show a || b
+Show a \/ b
+Show a ∨ b
+Show (or a b)
+Show or a (or a b)
+(* Simple Formulas *)
+Show a => b => a
+Check a => b
+Eval a => a
+Eval true => a
+(* Simple proof *)
+Axiom H1 : a
+Axiom H2 : a => b
+Check MP
+Show MP a b H2 H1
+Check MP a b H2 H1