diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index 043060dc63f2c1d79409e649dc8fc9cc4440d52f..b879f5b5f7c799e9c4eb86483cf2b7bad8feddc5 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -424,4 +424,24 @@ mod tests {
         );
         assert!(ty.conversion(&Type(0.into()), &Environment::new(), 0.into()))
     }
+
+    #[test]
+    fn prod_var() {
+        let ty = Prod(box Prop, box Prod(box Var(1.into()), box Var(2.into())));
+        let t = Abs(box Prop, box Abs(box Var(1.into()), box Var(1.into())));
+        assert!(t.check(&ty, &Environment::new()).is_ok())
+    }
+
+    #[test]
+    fn univ_reduc() {
+        let ty = App(
+            box Abs(box Prop, box Type(BigUint::from(0_u64).into())),
+            box Prod(box Prop, box Var(1.into())),
+        );
+        assert!(ty.conversion(
+            &Type(BigUint::from(0_u64).into()),
+            &Environment::new(),
+            0.into()
+        ))
+    }
 }