diff --git a/sol-driver/suite/church_encoding/church_encoding.expect b/sol-driver/suite/church_encoding/church_encoding.expect
index e69de29..b5bb05b 100644
--- a/sol-driver/suite/church_encoding/church_encoding.expect
+++ b/sol-driver/suite/church_encoding/church_encoding.expect
@@ -0,0 +1,34 @@
+
+// Natural numbers
+Nat
+  : U
+  = (n : U) -> (n -> n) -> n
+
+Succ
+  : Nat -> Nat
+  = |prev n succ$ zero$| succ$ (prev n succ$ zero$) zero$
+
+Zero
+  : Nat
+  = |n succ$ zero$| zero$
+
+// Maybe definition
+Maybe
+  : U -> U
+  = |t| (a : U) -> (t -> a) -> a -> a
+
+Just
+  : {a : U} -> a -> Maybe a
+  = |value t just$ nothing$| just$ value
+
+Nothing
+  : {a : U} -> Maybe a
+  = |t just$ nothing$| nothing$
+
+Sorry
+  : {a : U} -> a
+  = Sorry
+
+Maybe.unwrap : {a : U} -> Maybe a -> a
+Maybe.unwrap = |maybe|
+  maybe (|value| value) Sorry
diff --git a/sol-driver/suite/church_encoding/leibniz_equality.expect b/sol-driver/suite/church_encoding/leibniz_equality.expect
index e69de29..14d963d 100644
--- a/sol-driver/suite/church_encoding/leibniz_equality.expect
+++ b/sol-driver/suite/church_encoding/leibniz_equality.expect
@@ -0,0 +1,11 @@
+Eq
+  : {a : U} -> a -> a -> U
+  = |a x y| (p : a -> U) -> p x -> p y
+
+Eq.refl
+  : {a : U} -> {x : a} -> Eq a a
+  = |a px| px
+
+Test_Eq_Int64_10_10
+  : Eq 10 10
+  = Eq.refl