diff --git a/StdLib/Char.gr b/StdLib/Char.gr
deleted file mode 100644
index 216036846..000000000
--- a/StdLib/Char.gr
+++ /dev/null
@@ -1,30 +0,0 @@
-import Either
-
-digitToInt : Char -> Either Char Int
-digitToInt c = case charToInt c - 48 of
-  0 -> Right 0;
-  1 -> Right 1;
-  2 -> Right 2;
-  3 -> Right 3;
-  4 -> Right 4;
-  5 -> Right 5;
-  6 -> Right 6;
-  7 -> Right 7;
-  8 -> Right 8;
-  9 -> Right 9;
-  c -> Left c
-
-
--- Don't have Char literal patterns
--- digitToInt : Char -> Maybe Int
--- digitToInt '0' = Some 0;
--- digitToInt '1' = Some 1;
--- digitToInt '2' = Some 2;
--- digitToInt '3' = Some 3;
--- digitToInt '4' = Some 4;
--- digitToInt '5' = Some 5;
--- digitToInt '6' = Some 6;
--- digitToInt '7' = Some 7;
--- digitToInt '8' = Some 8;
--- digitToInt '9' = Some 9;
--- digitToInt c = None;
\ No newline at end of file
diff --git a/StdLib/Nat.gr b/StdLib/Nat.gr
index 5738663c3..1ab012234 100644
--- a/StdLib/Nat.gr
+++ b/StdLib/Nat.gr
@@ -48,12 +48,3 @@ mult_r [n] (S m') = add n (mult_r [n] m')
 div2 : forall {n : Nat} . N (2 * n) -> N n
 div2 Z = Z;
 div2 (S (S x)) = S (div2 x)
-
---- Existential nat
-data NX where
-  NX : ∀ {n : Nat} . N n → NX
-
-
-natToNX : Int → NX
-natToNX 0 = NX Z;
-natToNX n = let (NX m) = natToNX (n - 1) in NX (S m)
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/CrossDefPolymorphism.gr.output b/frontend/tests/cases/negative/CrossDefPolymorphism.gr.output
new file mode 100644
index 000000000..817fd681b
--- /dev/null
+++ b/frontend/tests/cases/negative/CrossDefPolymorphism.gr.output
@@ -0,0 +1,3 @@
+Type checking failed: 
+  Unification failed: 6:7:
+  Cannot unify universally quantified type variable `s`` of kind `Type` with a concrete type `s [2]`
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/approximation2.gr.output b/frontend/tests/cases/negative/approximation2.gr.output
index 5e7055394..f8432e886 100644
--- a/frontend/tests/cases/negative/approximation2.gr.output
+++ b/frontend/tests/cases/negative/approximation2.gr.output
@@ -1,4 +1,4 @@
 Type checking failed: 
   Falsifiable theorem: 5:1:
   The following theorem associated with `borg` is falsifiable:
-	(prom_[x]0 + prom_[x] ≤ 5..6) ∧ (3..4 ≤ prom_[x]) ∧ (0..1 ≤ prom_[x]0)
\ No newline at end of file
+	( -> (prom_[x]1 * 1 : Interval Nat + prom_[x]0 * 1 : Interval Nat ≤ 5..6) ∧ (3..4 ≤ prom_[x]0) ∧ (0..1 ≤ prom_[x]1))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/badExistential.gr.output b/frontend/tests/cases/negative/badExistential.gr.output
index 3448a1666..a0f541477 100644
--- a/frontend/tests/cases/negative/badExistential.gr.output
+++ b/frontend/tests/cases/negative/badExistential.gr.output
@@ -1,3 +1,3 @@
 Type checking failed: 
   Type error: 4:23:
-  Expected `f t -> a` but got `f a -> a`
\ No newline at end of file
+  Expected `f t -> a` but got `f a0.0 -> a`
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/badExistential2.gr.output b/frontend/tests/cases/negative/badExistential2.gr.output
index 1081c3ec5..570be6e0b 100644
--- a/frontend/tests/cases/negative/badExistential2.gr.output
+++ b/frontend/tests/cases/negative/badExistential2.gr.output
@@ -1,3 +1,3 @@
 Type checking failed: 
   Operator resolution failed: 6:14:
-  Could not resolve operator `+` at type `a -> Int -> ..`
\ No newline at end of file
+  Could not resolve operator `+` at type `a0.0 -> Int -> ..`
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/badIndexingMatch.gr.output b/frontend/tests/cases/negative/badIndexingMatch.gr.output
new file mode 100644
index 000000000..82e2a6ac9
--- /dev/null
+++ b/frontend/tests/cases/negative/badIndexingMatch.gr.output
@@ -0,0 +1,3 @@
+Type checking failed: 
+  Unification failed: 7:11:
+  Cannot unify universally quantified type variable `a`` of kind `Type` with a concrete type `Maybe t1.0`
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/badPoly.gr.output b/frontend/tests/cases/negative/badPoly.gr.output
index 33b32ab95..b0edc57e4 100644
--- a/frontend/tests/cases/negative/badPoly.gr.output
+++ b/frontend/tests/cases/negative/badPoly.gr.output
@@ -1,3 +1,3 @@
 Type checking failed: 
   Type error: 2:14:
-  Expected `a -> a -> (a, b)` but got `a -> b -> (a, b)`
\ No newline at end of file
+  Expected `a -> a -> (a, b)` but got `a0 -> b0 -> (a0, b0)`
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/badRecursiveArgument.gr.output b/frontend/tests/cases/negative/badRecursiveArgument.gr.output
new file mode 100644
index 000000000..5b4000e71
--- /dev/null
+++ b/frontend/tests/cases/negative/badRecursiveArgument.gr.output
@@ -0,0 +1,4 @@
+Type checking failed: 
+  Counter example: 7:1:
+  The following theorem associated with `fibble` is falsifiable:
+	∀ [(n0.0, ↑Nat),(t1.0, ↑Nat)] . ((t1.0 = n0.0 + 1) ∧ (n = t1.0) -> (n1 = n1 + 1) ∧ (n0.0 = n1))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/bool.gr.output b/frontend/tests/cases/negative/bool.gr.output
index 146fc56c8..f9aeb4557 100644
--- a/frontend/tests/cases/negative/bool.gr.output
+++ b/frontend/tests/cases/negative/bool.gr.output
@@ -1,3 +1,3 @@
 Type checking failed: 
-  Wrong return type in data constructor: 2:3:
+  Wrong return type in value constructor: 2:3:
   Expected type constructor `Bool`, but got `Int`
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/cartesianCase.gr.output b/frontend/tests/cases/negative/cartesianCase.gr.output
index 0072466da..770974886 100644
--- a/frontend/tests/cases/negative/cartesianCase.gr.output
+++ b/frontend/tests/cases/negative/cartesianCase.gr.output
@@ -1,4 +1,3 @@
 Type checking failed: 
-  Falsifiable theorem: 5:1:
-  The following theorem associated with `foo` is falsifiable:
-	(1 ≤ ∞) ∧ (1 ≤ ∞)
\ No newline at end of file
+  Pattern match impossible: 8:6:
+  Pattern match in an equation of `case` is impossible as it implies the unsatisfiable condition (1 ≤ ∞)
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/case.gr.output b/frontend/tests/cases/negative/case.gr.output
index e10830a5b..4f1472c8b 100644
--- a/frontend/tests/cases/negative/case.gr.output
+++ b/frontend/tests/cases/negative/case.gr.output
@@ -1,4 +1,2 @@
-Type checking failed: 
-  Counter example: 5:1:
-  The following theorem associated with `foo` is falsifiable:
-	(0 ≤ n) ∧ ∀ n.80,t.53 . ((0 ≤ 0) ∧ (n = n80 + 1) ∧ ∃ t52 : Type . ¬((n = 0)) -> (0 ≤ n) ∧ (n81 + 1 ≤ n) ∧ (0 ≤ 0) ∧ (n80 = n81)) ∧ ∀ t.52 . ((n = 0) -> (0 ≤ n))
\ No newline at end of file
+Parse error: 
+  lexical error at line 4, column 61
diff --git a/frontend/tests/cases/negative/disallowZeroBoundFromUnifyingPatterns.gr.output b/frontend/tests/cases/negative/disallowZeroBoundFromUnifyingPatterns.gr.output
index bff3c6e6d..7881b8b31 100644
--- a/frontend/tests/cases/negative/disallowZeroBoundFromUnifyingPatterns.gr.output
+++ b/frontend/tests/cases/negative/disallowZeroBoundFromUnifyingPatterns.gr.output
@@ -1,3 +1,3 @@
 Type checking failed: 
-  Grading error: 9:6:
-  1 is not approximatable by 0 for type Nat because Nat denotes precise usage.
\ No newline at end of file
+  Pattern match impossible: 9:5:
+  Pattern match in an equation of `case` is impossible as it implies the unsatisfiable condition (1 ≤ 0)
diff --git a/frontend/tests/cases/negative/everyOtherBroken.gr.output b/frontend/tests/cases/negative/everyOtherBroken.gr.output
index 50cba78ca..c67de46b9 100644
--- a/frontend/tests/cases/negative/everyOtherBroken.gr.output
+++ b/frontend/tests/cases/negative/everyOtherBroken.gr.output
@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 8:1:
   The following theorem associated with `everyOther` is falsifiable:
-	∀ n,a.1,n.0,a.2 . ((0..0 ≤ 0..1) ∧ (n + 1 = n0 + 1 + 1) ∧ ∃ a : Type . ¬((n + 1 = 0)) -> (1..1 ≤ 0..1) ∧ (1 + n2 ≤ n + 1) ∧ (n1 + 1 = n1 + 1 + 1) ∧ (n2 = n1) ∧ (0..1 ≤ 0..1) ∧ (n1 = n2))
\ No newline at end of file
+	∀ [(n0.0, ↑Nat),(a1.0, Type),(t2.0, Type),(t3.0, ↑Nat),(n0.1, ↑Nat),(a1.1, Type),(t2.1, Type),(t3.1, ↑Nat)] . ((0 : Interval Nat ≤ 0..1) ∧ (t3.1 = n0.1 + 1) ∧ (t3.1 = n0.0) ∧ (t3.0 = n0.0 + 1) ∧ (n = t3.0) -> (1 : Interval Nat ≤ 0..1) ∧ (1 + n1 * 1 ≤ n) ∧ (n0.2 + 1 = n0.0 + 1) ∧ (n1 = n0.2) ∧ (0..1 ≤ 0..1) ∧ (n0.1 = n1))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/everyOtherBroken2.gr.output b/frontend/tests/cases/negative/everyOtherBroken2.gr.output
index d16da5858..ac92936da 100644
--- a/frontend/tests/cases/negative/everyOtherBroken2.gr.output
+++ b/frontend/tests/cases/negative/everyOtherBroken2.gr.output
@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 9:1:
   The following theorem associated with `everyOther` is falsifiable:
-	∀ a.1,n,a.2,n.0 . ((0..0 ≤ 0..1) ∧ (n + 1 = n0 + 1 + 1) ∧ ∃ a : Type . ¬((n + 1 = 0)) -> (1..1 ≤ 0..1) ∧ (1 + n2 ≤ n + 1) ∧ (n1 + 1 = n1 + 1 + 1) ∧ (n2 = n1) ∧ (0..1 ≤ 0..1) ∧ (n1 = n2))
\ No newline at end of file
+	∀ [(a1.0, Type),(n0.0, ↑Nat),(t2.0, Type),(t3.0, ↑Nat),(a1.1, Type),(n0.1, ↑Nat),(t2.1, Type),(t3.1, ↑Nat)] . ((0 : Interval Nat ≤ 0..1) ∧ (t3.1 = n0.1 + 1) ∧ (t3.1 = n0.0) ∧ (t3.0 = n0.0 + 1) ∧ (n = t3.0) -> (1 : Interval Nat ≤ 0..1) ∧ (1 + n1 * 1 ≤ n) ∧ (n0.2 + 1 = n0.0 + 1) ∧ (n1 = n0.2) ∧ (0..1 ≤ 0..1) ∧ (n0.1 = n1))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/fact-inf.gr.output b/frontend/tests/cases/negative/fact-inf.gr.output
index fcd5ed21c..59227bcd0 100644
--- a/frontend/tests/cases/negative/fact-inf.gr.output
+++ b/frontend/tests/cases/negative/fact-inf.gr.output
@@ -1,4 +1,3 @@
 Type checking failed: 
-  Counter example: 4:1:
-  The following theorem associated with `fact` is falsifiable:
-	(1..1 ≤ ∞..∞)
\ No newline at end of file
+  Pattern match impossible: 5:1:
+  Pattern match in an equation of `fact` is impossible as it implies the unsatisfiable condition (t1.13 = n0.13 + 1) ∧ (n = t1.13) ∧ (1 : Interval (Ext Nat) ≤ ∞..∞)
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/flat.gr.output b/frontend/tests/cases/negative/flat.gr.output
index ed19502e9..8583bb6ba 100644
--- a/frontend/tests/cases/negative/flat.gr.output
+++ b/frontend/tests/cases/negative/flat.gr.output
@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 2:1:
   The following theorem associated with `flatten` is falsifiable:
-	(1 ≤ d + 1) ∧ ((c + 1) * (d + 1) = c + 1)
\ No newline at end of file
+	( -> (1 ≤ d + 1) ∧ ( -> (((c + 1) * (d + 1)) * 1 = c + 1)))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/flatten/flattenByLet.gr.output b/frontend/tests/cases/negative/flatten/flattenByLet.gr.output
index 46e051445..bfcebe16d 100644
--- a/frontend/tests/cases/negative/flatten/flattenByLet.gr.output
+++ b/frontend/tests/cases/negative/flatten/flattenByLet.gr.output
@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 2:1:
   The following theorem associated with `flatten` is falsifiable:
-	(m * n = m * n)
\ No newline at end of file
+	( -> ( -> (1 = n) ∧ ( -> ((m * n) * 1 = m))))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/flatten/flattenLevel.gr.output b/frontend/tests/cases/negative/flatten/flattenLevel.gr.output
index db8fe7ee7..3c7d01c72 100644
--- a/frontend/tests/cases/negative/flatten/flattenLevel.gr.output
+++ b/frontend/tests/cases/negative/flatten/flattenLevel.gr.output
@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 2:1:
   The following theorem associated with `flattenLevel` is falsifiable:
-	(k /\ l ≤ l \/ k)
\ No newline at end of file
+	( -> ((k /\ l) * 1 : Level ≤ l \/ k))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/flatten/flattenNat.gr.output b/frontend/tests/cases/negative/flatten/flattenNat.gr.output
index f1f2ac480..71264a495 100644
--- a/frontend/tests/cases/negative/flatten/flattenNat.gr.output
+++ b/frontend/tests/cases/negative/flatten/flattenNat.gr.output
@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 2:1:
   The following theorem associated with `flattenNat` is falsifiable:
-	(m + n ≤ n * m)
\ No newline at end of file
+	( -> ((m + n) * 1 ≤ n * m))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/headAlt.gr.output b/frontend/tests/cases/negative/headAlt.gr.output
index 793007368..7c72e1661 100644
--- a/frontend/tests/cases/negative/headAlt.gr.output
+++ b/frontend/tests/cases/negative/headAlt.gr.output
@@ -1,3 +1,3 @@
 Type checking failed: 
-  Pattern unreachable: 6:1:
-  Pattern guard for equation of `headAlt` is impossible. Its condition is Falsifiable
\ No newline at end of file
+  Pattern match impossible: 6:1:
+  Pattern match in an equation of `headAlt` is impossible as it implies the unsatisfiable condition (t1.0 = 0) ∧ (n = t1.0) ∧ (1 : Interval Nat ≤ 0..1) ∧ (n > 0)
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/headAlt2.gr.output b/frontend/tests/cases/negative/headAlt2.gr.output
index a4373271f..d180412ff 100644
--- a/frontend/tests/cases/negative/headAlt2.gr.output
+++ b/frontend/tests/cases/negative/headAlt2.gr.output
@@ -1,4 +1,4 @@
 Type checking failed: 
   Falsifiable theorem: 10:1:
   The following theorem associated with `foo` is falsifiable:
-	(0..1 ≤ 0..1) ∧ (0 > 0)
\ No newline at end of file
+	( -> (n1 = 0) ∧ (0..1 ≤ 0..1) ∧ (n1 > 0))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/headAlt3.gr.output b/frontend/tests/cases/negative/headAlt3.gr.output
index a4976e9c2..b128ad547 100644
--- a/frontend/tests/cases/negative/headAlt3.gr.output
+++ b/frontend/tests/cases/negative/headAlt3.gr.output
@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 9:1:
   The following theorem associated with `headAlt'` is falsifiable:
-	((n > 0) -> (n = n0) ∧ (0..1 ≤ 0..1) ∧ (n > 1))
\ No newline at end of file
+	((n > 0) -> (n = n1) ∧ (0..1 ≤ 0..1) ∧ (n1 > 1))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/impossiblePat.gr.output b/frontend/tests/cases/negative/impossiblePat.gr.output
index 7882c0fbb..cd5733f84 100644
--- a/frontend/tests/cases/negative/impossiblePat.gr.output
+++ b/frontend/tests/cases/negative/impossiblePat.gr.output
@@ -1,3 +1,4 @@
 Type checking failed: 
-  Pattern unreachable: 6:1:
-  Pattern guard for equation of `last` is impossible. Its condition is Falsifiable
\ No newline at end of file
+  Counter example: 8:1:
+  The following theorem associated with `last` is falsifiable:
+	∀ [(n0.1, ↑Nat),(t3.1, Type),(t4.1, Type),(t5.1, ↑Nat)] . ((0 : Interval Nat ≤ 0..1) ∧ (t5.1 = n0.1 + 1) ∧ (t5.1 = n + 1) -> (0..1 ≤ 0..1) ∧ (n0.1 = n1 + 1))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/noConsumption.gr.output b/frontend/tests/cases/negative/noConsumption.gr.output
index 7e7043fc6..f2cc2ffc7 100644
--- a/frontend/tests/cases/negative/noConsumption.gr.output
+++ b/frontend/tests/cases/negative/noConsumption.gr.output
@@ -1,5 +1,4 @@
 Type checking failed: 
-  Pattern unreachable: 4:1:
-  Pattern guard for equation of `and` is impossible.
-	0 is not approximatable by 1 for type Nat because Nat denotes precise usage.
-	0 is not approximatable by 1 for type Nat because Nat denotes precise usage.
\ No newline at end of file
+  Pattern match impossible: 4:1:
+  Pattern match in an equation of `and` is impossible as it implies the unsatisfiable condition (0 ≤ 1)
+(0 ≤ 1)
diff --git a/frontend/tests/cases/negative/polarity.gr.output b/frontend/tests/cases/negative/polarity.gr.output
index bca445792..c8ef4afeb 100644
--- a/frontend/tests/cases/negative/polarity.gr.output
+++ b/frontend/tests/cases/negative/polarity.gr.output
@@ -1,7 +1,7 @@
 Type checking failed: 
   Unification failed: 3:40:
-  Trying to match a polymorphic type  `a` with monomorphic type `a [0]`
+  Cannot unify universally quantified type variable `a`` of kind `Type` with a concrete type `a [0]`
 
 Falsifiable theorem: 7:1:
   The following theorem associated with `secondOrderAlt` is falsifiable:
-	(prom_[x] ≤ 0) ∧ (prom_[x] ≤ 1)
\ No newline at end of file
+	( -> (prom_[x]0 * 1 ≤ 0) ∧ (prom_[x]0 ≤ 1))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/poly.gr.output b/frontend/tests/cases/negative/poly.gr.output
index a567f9909..3958f1273 100644
--- a/frontend/tests/cases/negative/poly.gr.output
+++ b/frontend/tests/cases/negative/poly.gr.output
@@ -1,3 +1,3 @@
 Type checking failed: 
   Unification failed: 2:9:
-  Type `Int` is not unifiable with `a`
\ No newline at end of file
+  Cannot unify universally quantified type variable `a`` of kind `Type` with a concrete type `Int`
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/predicateFalseInDef.gr.output b/frontend/tests/cases/negative/predicateFalseInDef.gr.output
index 793007368..7c72e1661 100644
--- a/frontend/tests/cases/negative/predicateFalseInDef.gr.output
+++ b/frontend/tests/cases/negative/predicateFalseInDef.gr.output
@@ -1,3 +1,3 @@
 Type checking failed: 
-  Pattern unreachable: 6:1:
-  Pattern guard for equation of `headAlt` is impossible. Its condition is Falsifiable
\ No newline at end of file
+  Pattern match impossible: 6:1:
+  Pattern match in an equation of `headAlt` is impossible as it implies the unsatisfiable condition (t1.0 = 0) ∧ (n = t1.0) ∧ (1 : Interval Nat ≤ 0..1) ∧ (n > 0)
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/predicateFalseInUse.gr.output b/frontend/tests/cases/negative/predicateFalseInUse.gr.output
index b38e3e6e5..5358bc4a6 100644
--- a/frontend/tests/cases/negative/predicateFalseInUse.gr.output
+++ b/frontend/tests/cases/negative/predicateFalseInUse.gr.output
@@ -1,4 +1,4 @@
 Type checking failed: 
   Falsifiable theorem: 9:1:
   The following theorem associated with `foo` is falsifiable:
-	(0..1 ≤ 0..1) ∧ (0 > 0)
\ No newline at end of file
+	( -> (n1 = 0) ∧ (0..1 ≤ 0..1) ∧ (n1 > 0))
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/universal.gr.output b/frontend/tests/cases/negative/universal.gr.output
index d055abf3a..02f93a4a3 100644
--- a/frontend/tests/cases/negative/universal.gr.output
+++ b/frontend/tests/cases/negative/universal.gr.output
@@ -1,4 +1,4 @@
 Type checking failed: 
   Counter example: 2:1:
   The following theorem associated with `foo` is falsifiable:
-	(2 ≤ n)
\ No newline at end of file
+	( -> (1 + 1 ≤ n))
\ No newline at end of file
diff --git a/StdLib/Choice.gr b/work-in-progress/Choice.gr
similarity index 84%
rename from StdLib/Choice.gr
rename to work-in-progress/Choice.gr
index ca41bce45..ab0a205a7 100644
--- a/StdLib/Choice.gr
+++ b/work-in-progress/Choice.gr
@@ -40,5 +40,11 @@
 data Choice : Type -> Type -> Nat -> Type where
   MkChoice : forall {a : Type, b : Type,  m : Nat,  n : Nat}. a [0..m] -> b [0..n] -> Choice a b (m + n)
 
-chooseA : forall {a : Type, b : Type,  m : Nat,  n : Nat}. Choice a b (n + 1) -> (a, Choice a b n)
+chooseA : forall {a : Type, b : Type, n : Nat}. Choice a b (n + 1) -> (a, Choice a b n)
 chooseA (MkChoice [a] [b]) = (a, MkChoice [a] [b])
+
+chooseLeft : forall {a : Type, b : Type,  m : Nat,  n : Nat}. Choice a b 1 -> a
+chooseLeft (MkChoice [a] [_]) = a
+
+chooseRight : forall {a : Type, b : Type,  m : Nat,  n : Nat}. Choice a b 1 -> b
+chooseRight (MkChoice [_] [b]) = b
diff --git a/work-in-progress/existentialNat.gr b/work-in-progress/existentialNat.gr
new file mode 100644
index 000000000..1a6a6f73d
--- /dev/null
+++ b/work-in-progress/existentialNat.gr
@@ -0,0 +1,11 @@
+import Nat
+
+-- Recent changes means this doesn't work
+
+--- Existential nat
+data NX where
+  NX : ∀ {n : Nat} . N n → NX
+
+natToNX : Int → NX
+natToNX 0 = NX Z;
+natToNX n = let (NX m) = natToNX (n - 1) in NX (S m)