diff --git a/code/Decidability/DiscreteTypes.v b/code/Decidability/DiscreteTypes.v
index 02b19c0..c5c356d 100644
--- a/code/Decidability/DiscreteTypes.v
+++ b/code/Decidability/DiscreteTypes.v
@@ -1,4 +1,7 @@
 Require Import init.imports.
+Require Import UniMath.Combinatorics.Lists.
+Require Import UniMath.Combinatorics.MoreLists.
+Require Import Inductive.Option.
   
 Section EqualityDeciders.
 
@@ -138,12 +141,4 @@ Section ClosureProperties.
         * exact inr.
   Qed.
 
-
-  
-  
-End ClosureProperties.
-
-
-Section ChoiceFunction.
-
-End ChoiceFunction.
+End ClosureProperties.
\ No newline at end of file
diff --git a/code/Inductive/Option.v b/code/Inductive/Option.v
index 99db353..a659ca6 100644
--- a/code/Inductive/Option.v
+++ b/code/Inductive/Option.v
@@ -1,5 +1,5 @@
-(* Definition of an option as the coproduct of a type X with the unit type *)
 
+(* Definition of an option as the coproduct of a type X with the unit type *)
 Require Import init.imports. 
 
 Section Option.
@@ -10,3 +10,23 @@ Section Option.
   Definition none {X : UU} : @option X := (ii2 tt).
   
 End Option.
+
+Section PathProperties.
+
+  Lemma nopathssomenone {X : UU} (x : X) : ¬ ((some x) = none). 
+  Proof.
+    apply negpathsii1ii2.
+  Qed.
+
+  Lemma nopathsnonesome {X : UU} (x : X) : ¬ (none = (some x)).
+  Proof.
+    apply negpathsii2ii1.
+  Qed.
+
+  Lemma some_injectivity {X : UU} (x y : X) : (some x = some y) → x = y.
+  Proof.
+    apply ii1_injectivity.
+  Qed.
+  
+  
+End PathProperties.
diff --git a/code/_CoqProject b/code/_CoqProject
index cae6f3c..7b30385 100644
--- a/code/_CoqProject
+++ b/code/_CoqProject
@@ -2,11 +2,13 @@ COQC = coqc
 COQDEP = coqdep
 -R . "sem"
 
+
 -arg "-w -notation-overridden -type-in-type -noinit"
 
 init/imports.v
 init/all.v
 
+
 Inductive/ListProperties.v
 Inductive/Option.v