diff --git a/stdlib/prop.rkt b/stdlib/prop.rkt
index c92889d..998eaa2 100644
--- a/stdlib/prop.rkt
+++ b/stdlib/prop.rkt
@@ -62,5 +62,23 @@
 
 (qed thm:proj2 proof:proj2)
 
+(data Or : (forall* (A : Type) (B : Type) Type)
+  (left : (forall* (A : Type) (B : Type) (a : A) (Or A B)))
+  (right : (forall* (A : Type) (B : Type) (b : B) (Or A B))))
+
+(define-theorem thm:A-or-A
+  (forall* (A : Type) (o : (Or A A)) A))
+
+(define proof:A-or-A
+  (lambda* (A : Type) (c : (Or A A))
+    ;; TODO: What should the motive be?
+    (elim Or Type (lambda* (A : Type) (B : Type) (c : (Or A B)) A)
+      (lambda* (A : Type) (B : Type) (a : A) a)
+      ;; TODO: How do we know B is A?
+      (lambda* (A : Type) (B : Type) (b : B) b)
+      A A c)))
+
+(qed thm:A-or-A proof:A-or-A)
+
 (data == : (forall* (A : Type) (x : A) (-> A Type))
   (refl : (forall* (A : Type) (x : A) (== A x x))))