1 files changed, 1 insertions, 1 deletions

diff --git a/HoTT.thy b/HoTT.thy
index abb1085..3f2d475 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -30,7 +30,7 @@ begin
 lemmas forms =
   Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form
 lemmas intros =
-  Nat_intro Prod_intro Sum_intro Equal_intro Coprod_intro Unit_intro
+  Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro
 lemmas elims =
   Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim
 lemmas routines =