diff --git a/kernel/src/command.rs b/kernel/src/command.rs
index 39402a2d5f2c795e04e064eae5bde0e448baeca2..570ee1e98852a03cdb8cfbd1e6a2fb87bc2ccfff 100644
--- a/kernel/src/command.rs
+++ b/kernel/src/command.rs
@@ -17,11 +17,11 @@ impl Command {
         match self {
             Command::Define(s, None, term) => term
                 .infer(env)
-                .and_then(|t| env.insert(s, term, t).map(|_| None)),
+                .and_then(|t| env.insert_def(s, term, t).map(|_| None)),
 
             Command::Define(s, Some(t), term) => term
                 .check(&t, env)
-                .and_then(|_| env.insert(s, term, t).map(|_| None)),
+                .and_then(|_| env.insert_def(s, term, t).map(|_| None)),
 
             Command::CheckType(t1, t2) => t1.check(&t2, env).map(|_| None),
 
@@ -38,7 +38,7 @@ mod tests {
 
     fn simple_env() -> Environment {
         Environment::new()
-            .insert("x".to_string(), Term::r#type(0.into()), Term::PROP)
+            .insert_def("x".to_string(), Term::r#type(0.into()), Term::PROP)
             .unwrap()
             .clone()
     }
@@ -61,7 +61,7 @@ mod tests {
         assert_eq!(
             env,
             *(simple_env()
-                .insert("y".to_string(), Term::PROP, Term::r#type(0.into()))
+                .insert_def("y".to_string(), Term::PROP, Term::r#type(0.into()))
                 .unwrap())
         );
     }
@@ -84,7 +84,7 @@ mod tests {
         assert_eq!(
             env,
             *(simple_env()
-                .insert("y".to_string(), Term::PROP, Term::r#type(0.into()))
+                .insert_def("y".to_string(), Term::PROP, Term::r#type(0.into()))
                 .unwrap())
         );
     }
diff --git a/kernel/src/environment.rs b/kernel/src/environment.rs
index 5096eacde0998c2e77e58aff78a823795be3bf76..cd6e264e1eb66e9842100806bc8138f2219602a1 100644
--- a/kernel/src/environment.rs
+++ b/kernel/src/environment.rs
@@ -15,16 +15,26 @@ impl Environment {
         Self::default()
     }
 
-    /// Creates a new environment binding s with (t1,t2)
-    pub fn insert(&mut self, s: String, t1: Term, t2: Term) -> Result<&Self, KernelError> {
+    pub fn insert(&mut self, s: String, decl : Declaration) -> Result<&Self, KernelError> {
         if let hash_map::Entry::Vacant(e) = self.0.entry(s.clone()) {
-            e.insert(Declaration::make(Some(t1), t2));
+            e.insert(decl);
             Ok(self)
         } else {
             Err(KernelError::AlreadyDefined(s))
         }
     }
 
+    /// Creates a new environment binding s with t1 : t2
+    pub fn insert_def(&mut self, s: String, t1: Term, t2: Term) -> Result<&Self, KernelError> {
+        self.insert(s, Declaration::make(Some(t1), t2))
+    }
+
+    /// Creates a new environment binding s with an axiom of type ty
+    pub fn insert_axiom(&mut self, s: String, ty: Term) -> Result<&Self, KernelError> {
+        self.insert(s, Declaration::make(None, ty))
+    }
+    
+
     /// Returns the term linked to a definition in a given environment.
     pub fn get_term(&self, s: &String, vec: &[UniverseLevel]) -> Option<Term> {
         self.0.get(s).and_then(|decl| decl.get_term(vec))
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
index 03c332b1199f6557df70da51cb192cc0b4756080..e42e69338ada73e9702b03d2da24d2477cf5578e 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -383,7 +383,7 @@ mod tests {
             box Prod(box Var(1.into()), box Var(1.into())),
         );
         let mut env = Environment::new();
-        env.insert("foo".into(), id_prop.clone(), Sort(0.into()))
+        env.insert_def("foo".into(), id_prop.clone(), Sort(0.into()))
             .unwrap();
 
         assert_eq!(
@@ -408,7 +408,7 @@ mod tests {
         );
         assert!(id_te.check(&id_ty, &Environment::new()).is_ok());
         let mut binding = Environment::new();
-        let env = binding.insert("id".into(), id_te, id_ty).unwrap();
+        let env = binding.insert_def("id".into(), id_te, id_ty).unwrap();
         assert!(Const("id".into(), vec![0.into()])
             .is_def_eq(&id_zero, env)
             .is_ok())
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index fbe9b3d55023d1ad4832203cea3c57de9d95d16c..904ba83030c5c557972188df5b76317bcb6e6222 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -412,7 +412,7 @@ mod tests {
         );
         let mut binding = Environment::new();
         let env = binding
-            .insert("foo".into(), id_prop.clone(), Sort(0.into()))
+            .insert_def("foo".into(), id_prop.clone(), Sort(0.into()))
             .unwrap();
 
         assert!(t.check(&Const("foo".into(), Vec::new()), env).is_ok());
@@ -443,7 +443,7 @@ mod tests {
         );
         let mut binding = Environment::new();
         let env = binding
-            .insert("foo".into(), id_prop, Sort(0.into()))
+            .insert_def("foo".into(), id_prop, Sort(0.into()))
             .unwrap();
 
         assert!(Const("foo".into(), Vec::new()).infer(env).is_ok());