diff --git a/examples/inductives.gcic b/examples/inductives.gcic
index 5a3f5f2..c1ebf56 100644
--- a/examples/inductives.gcic
+++ b/examples/inductives.gcic
@@ -2,8 +2,8 @@ Inductive bool : Type :=
 | false : bool 
 | true : bool.
 
-Definition rec2 (c : Type@1) (fb tb : c) (b : bool) : c :=
-match@bool b as z return c with 
+Definition rec2 (c : bool -> Type@1) (fb : c false) (tb : c true) (b : bool) : c b :=
+match@bool b as z return c z with 
 | false => fb 
 | true => tb 
 end.
@@ -22,7 +22,7 @@ Inductive W (a : Type) (b : a -> Type) : Type@1 :=
 | sup (x : a) (f : b x -> W a b) : W a b.
 
 
-Definition natarity : bool -> Type := rec2 Type void unit.
+Definition natarity : bool -> Type := rec2 (fun (b : bool) => Type) void unit.
 
 Definition natW : Type@1 := W bool natarity.
 
@@ -41,3 +41,27 @@ match@sum s as z return c with
 | inl a b x => l x 
 | inr a b x => r x 
 end.
+
+Fixpoint recW (A : Type) (B : A -> Type) (E : W A B -> Type@1) 
+  (e : forall (x : A) (f : B x -> W A B) (rec : forall (b : B x), E (f b)), E (sup A B x f))
+  (w : W A B) {struct w} : E w :=
+match@W w as z return E z with
+| sup A B a f => e a f (fun (b : B a) => recW A B E e (f b))
+end.
+
+Definition recnatW (C : natW -> Type@1) 
+  (e : forall (x : bool) (f : natarity x -> W bool natarity) (rec : forall (b : natarity x), C (f b)), C (sup bool natarity x f))
+  (n : W bool natarity) : C n := recW bool natarity C e n.
+
+Definition double : natW -> natW :=
+recnatW (fun (x : natW) => natW) 
+  (rec2 (fun (b : bool ) =>
+    forall (f : natarity b -> natW)
+          (g : natarity b -> natW),
+          W bool natarity)
+        (fun (f : void -> natW)
+            (g : void -> natW) =>
+            zero)
+        (fun (f : unit -> natW)
+            (g : unit -> natW) =>
+            succ (succ (g tt)))).
diff --git a/examples/vector.gcic b/examples/vector.gcic
new file mode 100644
index 0000000..2b7a7f7
--- /dev/null
+++ b/examples/vector.gcic
@@ -0,0 +1,18 @@
+Inductive Nat : Type := 
+| O : Nat 
+| Succ (n : Nat) : Nat.
+
+Inductive unit : Type := | tt : unit. 
+
+Inductive prod (A B : Type) : Type := 
+| pair (a : A) (b : B) : prod A B.
+
+Fixpoint vec (A : Type) (n : Nat) {struct n} : Type := 
+    match@Nat n as z return Type with 
+    | O => unit 
+    | Succ m => prod A (vec A m) 
+    end.  
+
+Definition nil (A : Type) : vec A O := tt. 
+
+Definition cons (A : Type) (a : A) (n : Nat) (v : vec A n) : vec A (Succ n) := pair A (vec A n) a v.
\ No newline at end of file
diff --git a/lib/castCIC.ml b/lib/castCIC.ml
index 59ea20a..20efa1d 100644
--- a/lib/castCIC.ml
+++ b/lib/castCIC.ml
@@ -191,6 +191,44 @@ module Executor : Main.Executor = struct
       Const.add_cache name { name; ty = elab_ty; term = elab_term };
       Ok (Definition (name, ty))
 
+  let execute_fixpoint struct_id gdef : (cmd_result, execute_error) result =
+    let empty_ctx = Name.Map.empty in
+    match gdef with
+    | { name; ty; term } ->
+      let* rarg =
+        GCIC.prod_args ty
+        |> List.find_index_opt struct_id
+        |> Option.to_result
+             ~none:
+               (Format.asprintf
+                  "recursive argument not found: %s"
+                  (Name.to_string struct_id))
+      in
+      let* elab_ty, _ =
+        CastCICElab.elab_univ empty_ctx ty
+        |> Result.map_error Elaboration.Cast_CIC.string_of_error
+      in
+      let fix =
+        GCIC.Fixpoint { fix_id = name; fix_body = term; fix_type = ty; fix_rarg = rarg }
+      in
+      Const.add name { name; ty; term = fix };
+      Const.add_cache name { name; ty = elab_ty; term = Const name };
+      (* Temporary definition por typing *)
+      let* elab_term =
+        CastCICElab.check_elab empty_ctx term elab_ty
+        |> Result.map_error Elaboration.Cast_CIC.string_of_error
+      in
+      let elab_fix =
+        CastCIC.Fixpoint
+          { fix_id = name; fix_body = elab_term; fix_type = elab_ty; fix_rarg = rarg }
+      in
+      Const.add_cache name { name; ty = elab_ty; term = elab_fix };
+      let* _ =
+        CastCICTyping.check_type empty_ctx elab_term elab_ty
+        |> Result.map_error Typing.Cast_CIC.string_of_error
+      in
+      Ok (Definition (name, ty))
+
   let execute_inductive ind ctors : (cmd_result, execute_error) result =
     let empty_ctx = Name.Map.empty in
     let elab_univ_param (elab_params, ctx) (id, param) =
@@ -253,6 +291,7 @@ module Executor : Main.Executor = struct
     | Elab t -> execute_elab t
     | Set f -> execute_set_flag f
     | Define gdef -> execute_definition gdef
+    | Fix (struct_id, gdef) -> execute_fixpoint struct_id gdef
     | Load filename -> execute_load file_parser filename
     | Inductive (ind, ctors) -> execute_inductive ind ctors
 
diff --git a/lib/common/castCIC.ml b/lib/common/castCIC.ml
index 6690ede..c1dbd4f 100644
--- a/lib/common/castCIC.ml
+++ b/lib/common/castCIC.ml
@@ -41,6 +41,7 @@ type term =
       ; f : Name.t
       ; branches : branch list
       }
+  | Fixpoint of fix_info
 
 and fun_info =
   { id : Name.t
@@ -54,13 +55,25 @@ and branch =
   ; term : term
   }
 
+and fix_info =
+  { fix_id : Name.t
+  ; fix_body : term
+  ; fix_type : term
+  ; fix_rarg : int (* index of the recursive argument *)
+  }
+
+(** Checks if a term is a lambda expression *)
+let is_lambda = function
+  | Lambda _ -> true
+  | _ -> false
+
 (** Pretty printer *)
 module Pretty = struct
   open Fmt
 
   (** Returns if a term requires a parenthesis for unambiguation *)
   let need_parens = function
-    | Lambda _ | Prod _ | Cast _ | Match _ -> true
+    | App _ | Lambda _ | Prod _ | Cast _ | Match _ | Fixpoint _ -> true
     | Inductive (_, _, args) -> args <> []
     | Constructor { params; args; _ } -> params <> [] || args <> []
     | _ -> false
@@ -79,7 +92,7 @@ module Pretty = struct
     | Var x -> pf ppf "%a" Name.pp x
     | Universe 0 -> pf ppf "▢"
     | Universe i -> pf ppf "▢%i" i
-    | App (t, t') -> pf ppf "@[%a@ %a@]" maybe_parens t maybe_parens t'
+    | App (t, t') -> pf ppf "@[%a@ %a@]" maybe_parens_app t maybe_parens t'
     | Lambda _ as t -> group_lambda_args [] t |> pp_lambda ppf
     | Prod { id; dom; body } as t ->
       if Name.is_default id
@@ -98,6 +111,7 @@ module Pretty = struct
       pf ppf "@[%a@ %a@]" Name.pp ctor (list ~sep:sp maybe_parens) (params @ args)
     | Match { discr; z; pred; _ } ->
       pf ppf "@[match %a as %a return@ %a with@]" pp discr Name.pp z pp pred
+    | Fixpoint { fix_body; _ } -> pf ppf "@[fix@ %a@]" maybe_parens fix_body
 
   (** Pretty-prints an argument of a lambda or prod *)
   and pp_arg ppf (x, ty) = pf ppf "@[(%a : %a)@]" Name.pp x pp ty
@@ -111,7 +125,15 @@ module Pretty = struct
     pf ppf "@[<hov 1>∀%a,@ %a@]" (list ~sep:sp pp_arg) args pp body
 
   (** Adds parenthesis around a term if needed *)
-  and maybe_parens ppf t = if need_parens t then parens pp ppf t else pp ppf t
+  and maybe_parens ppf t =
+    match t with
+    | _ -> if need_parens t then parens pp ppf t else pp ppf t
+
+  (** Adds parenthesis around a term if needed *)
+  and maybe_parens_app ppf t =
+    match t with
+    | App _ -> pp ppf t
+    | _ -> if need_parens t then parens pp ppf t else pp ppf t
 
   (** Returns the prettified version of a term *)
   let to_string = to_to_string pp
@@ -170,6 +192,9 @@ let rec subst ctx = function
       ; pred = subst (Context.add mi.z (Var mi.z) ctx) mi.pred
       ; branches = List.map (subst_branch ctx) mi.branches
       }
+  | Fixpoint fi ->
+    Fixpoint
+      { fi with fix_body = subst ctx fi.fix_body; fix_type = subst ctx fi.fix_type }
 
 and subst_branch ctx br =
   let ids_ctx = List.map (fun x -> x, Var x) br.ids |> List.to_seq in
@@ -230,8 +255,15 @@ let rec alpha_equal t1 t2 =
     && m1.z = m2.z
     && alpha_equal m1.pred m2.pred
     && List.equal alpha_equal_branch m1.branches m2.branches
+  | Fixpoint fi1, Fixpoint fi2 -> alpha_equal_fix fi1 fi2
   | _ -> false
 
+and alpha_equal_fix fi1 fi2 =
+  fi1.fix_id = fi2.fix_id
+  && alpha_equal fi1.fix_body fi2.fix_body
+  && alpha_equal fi1.fix_type fi2.fix_type
+  && fi1.fix_rarg = fi2.fix_rarg
+
 let rec subst_tele ?(acc = []) ts params =
   match ts, params with
   | [], [] -> List.rev acc
diff --git a/lib/common/castCIC.mli b/lib/common/castCIC.mli
index 1dc542f..bf71808 100644
--- a/lib/common/castCIC.mli
+++ b/lib/common/castCIC.mli
@@ -36,6 +36,7 @@ type term =
       ; f : Name.t
       ; branches : branch list
       }
+  | Fixpoint of fix_info
 
 and fun_info =
   { id : Name.t
@@ -49,6 +50,16 @@ and branch =
   ; term : term
   }
 
+and fix_info =
+  { fix_id : Name.t
+  ; fix_body : term
+  ; fix_type : term
+  ; fix_rarg : int (* index of the recursive argument *)
+  }
+
+(** Checks if a term is a lambda expression *)
+val is_lambda : term -> bool
+
 (** Pretty printers *)
 val pp_term : Format.formatter -> term -> unit
 
diff --git a/lib/common/gCIC.ml b/lib/common/gCIC.ml
index 3002b33..b728b9b 100644
--- a/lib/common/gCIC.ml
+++ b/lib/common/gCIC.ml
@@ -24,6 +24,7 @@ type term =
   | Ascription of term * term
   | UnknownT of int
   | Const of Name.t
+  | Fixpoint of fix_info
 
 and fun_info =
   { id : Name.t
@@ -37,6 +38,13 @@ and branch =
   ; term : term
   }
 
+and fix_info =
+  { fix_id : Name.t
+  ; fix_body : term
+  ; fix_type : term
+  ; fix_rarg : int (* index of the recursive argument *)
+  }
+
 (** Pretty printers *)
 
 (** Pretty printer *)
@@ -45,7 +53,7 @@ module Pretty = struct
 
   (** Returns if a term requires a parenthesis for disambiguation *)
   let need_parens = function
-    | Lambda _ | Prod _ | Ascription _ | Match _ -> true
+    | Lambda _ | Prod _ | Ascription _ | Match _ | Fixpoint _ -> true
     | Inductive (_, _, args) | Constructor (_, args) -> args <> []
     | _ -> false
 
@@ -89,6 +97,7 @@ module Pretty = struct
     | Ascription (t, ty) -> pf ppf "@[%a ::@ %a@]" pp t pp ty
     | UnknownT i -> pf ppf "?▢%i" i
     | Const x -> pf ppf "%a" Name.pp x
+    | Fixpoint { fix_body; _ } -> pf ppf "@[fix@ %a@]" maybe_parens fix_body
 
   (** Pretty-prints an argument of a lambda or prod *)
   and pp_arg ppf (x, ty) = pf ppf "@[(%a : %a)@]" Name.pp x pp ty
@@ -143,8 +152,15 @@ let rec eq t1 t2 =
   | Ascription (t1, ty1), Ascription (t2, ty2) -> eq t1 t2 && eq ty1 ty2
   | UnknownT i, UnknownT j -> i = j
   | Const c1, Const c2 -> c1 = c2
+  | Fixpoint fi1, Fixpoint fi2 -> eq_fix fi1 fi2
   | _ -> false
 
+and eq_fix fi1 fi2 =
+  fi1.fix_id = fi2.fix_id
+  && eq fi1.fix_body fi2.fix_body
+  && eq fi1.fix_type fi2.fix_type
+  && fi1.fix_rarg = fi2.fix_rarg
+
 and branch_eq b1 b2 =
   b1.ctor = b2.ctor && List.equal ( = ) b1.ids b2.ids && eq b1.term b2.term
 
@@ -153,3 +169,7 @@ let rec get_universe_lvl (t : term) =
   | Universe lvl -> lvl
   | Prod fi -> get_universe_lvl fi.body
   | _ -> failwith "type of inductive definition must be a universe"
+
+let rec prod_args : term -> Name.t list = function
+  | Prod fi -> fi.id :: prod_args fi.body
+  | _ -> []
diff --git a/lib/common/gCIC.mli b/lib/common/gCIC.mli
index 7df8cd1..9a5458f 100644
--- a/lib/common/gCIC.mli
+++ b/lib/common/gCIC.mli
@@ -24,6 +24,7 @@ type term =
   | Ascription of term * term
   | UnknownT of int
   | Const of Name.t
+  | Fixpoint of fix_info
 
 and fun_info =
   { id : Name.t
@@ -37,6 +38,13 @@ and branch =
   ; term : term
   }
 
+and fix_info =
+  { fix_id : Name.t
+  ; fix_body : term
+  ; fix_type : term
+  ; fix_rarg : int (* index of the recursive argument *)
+  }
+
 (** Pretty printers *)
 val pp_term : Format.formatter -> term -> unit
 
@@ -52,3 +60,6 @@ val eq : term -> term -> bool
 (** Gets the level of a universe or a product.
     Raises an error if applied on something else. *)
 val get_universe_lvl : term -> int
+
+(** Returns the list of arguments of a product type. *)
+val prod_args : term -> Name.t list
diff --git a/lib/common/std.ml b/lib/common/std.ml
index 249909d..33378ce 100644
--- a/lib/common/std.ml
+++ b/lib/common/std.ml
@@ -38,4 +38,12 @@ module List = struct
       | _ -> List.rev acc, []
     in
     go [] n xs
+
+  let find_index_opt x xs =
+    let rec go acc xs =
+      match xs with
+      | [] -> None
+      | y :: ys -> if x = y then Some acc else go (acc + 1) ys
+    in
+    go 0 xs
 end
diff --git a/lib/elaboration/cast_CIC.ml b/lib/elaboration/cast_CIC.ml
index 3c2bcd1..dcf857a 100644
--- a/lib/elaboration/cast_CIC.ml
+++ b/lib/elaboration/cast_CIC.ml
@@ -170,7 +170,7 @@ module Make (ST : Store) (R : Reducer) : CastCICElab = struct
         then (
           let new_ids = List.map (fun _ -> Var (new_identifier ())) b1.ids in
           let ids1 = List.combine b1.ids new_ids in
-          let ids2 = List.combine b1.ids new_ids in
+          let ids2 = List.combine b2.ids new_ids in
           let subst_body body ids =
             List.fold_left
               (fun body (old_id, new_id) -> subst1 old_id new_id body)
@@ -186,6 +186,7 @@ module Make (ST : Store) (R : Reducer) : CastCICElab = struct
       && m1.ind = m2.ind
       && are_consistent m1.pred m2.pred
       && List.equal are_consistent_branch m1.branches m2.branches
+    | Fixpoint fi1, Fixpoint fi2 -> fi1.fix_id = fi2.fix_id
     | _ -> false
 
   (** The elaboration procedure, as per the paper *)
@@ -266,6 +267,19 @@ module Make (ST : Store) (R : Reducer) : CastCICElab = struct
         | Not_found -> Error (`Err_free_identifier x)
       in
       Ok (CastCIC.Const x, ty)
+    | Fixpoint fi ->
+      let* elab_fix_type, _ = elab_univ ctx fi.fix_type in
+      let fix_ctx = Name.Map.add fi.fix_id elab_fix_type ctx in
+      let* elab_fix_body = check_elab fix_ctx fi.fix_body elab_fix_type in
+      let elab_fix =
+        CastCIC.Fixpoint
+          { fix_id = fi.fix_id
+          ; fix_body = elab_fix_body
+          ; fix_type = elab_fix_type
+          ; fix_rarg = fi.fix_rarg
+          }
+      in
+      Ok (elab_fix, elab_fix_type)
 
   (* CHECK rule from the original paper *)
   and check_elab ctx term (s_ty : CastCIC.term) =
diff --git a/lib/main.ml b/lib/main.ml
index 4d2fd5c..ed7b313 100644
--- a/lib/main.ml
+++ b/lib/main.ml
@@ -139,6 +139,7 @@ module Make (E : Executor) : Run = struct
     | Elab t -> Elab (of_parsed_term t)
     | Set cfg -> Set cfg
     | Define d -> Define (of_parsed_const_decl d)
+    | Fix (rarg, d) -> Fix (rarg, of_parsed_const_decl d)
     | Load filename -> Load filename
     | Inductive (ind, ctors) ->
       let ind' = of_parsed_ind_decl ind in
diff --git a/lib/parsing/command.ml b/lib/parsing/command.ml
index a2c8269..d750962 100644
--- a/lib/parsing/command.ml
+++ b/lib/parsing/command.ml
@@ -8,5 +8,6 @@ type 'a t =
   | Elab of 'a
   | Set of Config.Flag.t
   | Define of 'a const_decl
+  | Fix of Common.Id.Name.t * 'a const_decl
   | Load of string
   | Inductive of 'a ind_decl * 'a ctor_decl list
diff --git a/lib/parsing/command.mli b/lib/parsing/command.mli
index a2c8269..d750962 100644
--- a/lib/parsing/command.mli
+++ b/lib/parsing/command.mli
@@ -8,5 +8,6 @@ type 'a t =
   | Elab of 'a
   | Set of Config.Flag.t
   | Define of 'a const_decl
+  | Fix of Common.Id.Name.t * 'a const_decl
   | Load of string
   | Inductive of 'a ind_decl * 'a ctor_decl list
diff --git a/lib/parsing/lexer.ml b/lib/parsing/lexer.ml
index cfba6b7..7bf62f2 100644
--- a/lib/parsing/lexer.ml
+++ b/lib/parsing/lexer.ml
@@ -47,6 +47,8 @@ let rec token lexbuf =
   | "Eval" -> VERNAC_EVAL
   | "Elab" -> VERNAC_ELABORATE
   | "Definition" -> VERNAC_DEFINITION
+  | "Fixpoint" -> VERNAC_FIXPOINT
+  | "struct" -> KWD_STRUCT
   | "Inductive" -> VERNAC_INDUCTIVE
   | "Set" -> VERNAC_SET
   | "Variant" -> VERNAC_FLAG_VARIANT
@@ -62,6 +64,8 @@ let rec token lexbuf =
   | big_arrow -> BIG_ARROW
   | '(' -> LPAREN
   | ')' -> RPAREN
+  | '{' -> LBRACE
+  | '}' -> RBRACE
   | ":=" -> ASSIGN
   | ':' -> COLON
   | ',' -> COMMA
diff --git a/lib/parsing/parser.mly b/lib/parsing/parser.mly
index ec49904..1c4b083 100644
--- a/lib/parsing/parser.mly
+++ b/lib/parsing/parser.mly
@@ -21,6 +21,14 @@
     let const_def = { name; ty; term } in
     Define const_def
 
+  let mk_fix name args struct_id ty' body =
+    let open Command in
+    let open Common.Declarations in
+    let term = Lambda (args, Ascription (body, ty')) in
+    let ty  = Prod (args, ty') in
+    let const_def = { name; ty; term } in
+    Fix (struct_id, const_def)
+
   (* The inductive's parameters are included immediately in the constructors during parsing *)
   let mk_ind_decl ind params' sort ctors =
     let open Command in
@@ -46,12 +54,12 @@
 %token <int> INT
 %token <string> ID FILENAME
 %token COLON COMMA ARROW BIG_ARROW VBAR AT ASSIGN
-%token LPAREN RPAREN
+%token LPAREN RPAREN LBRACE RBRACE
 %token KWD_UNIVERSE KWD_LAMBDA KWD_UNKNOWN KWD_UNKNOWN_T KWD_FORALL
-%token KWD_LET KWD_IN
+%token KWD_LET KWD_IN KWD_STRUCT
 %token KWD_MATCH KWD_AS KWD_RETURN KWD_WITH KWD_END
 %token VERNAC_CHECK VERNAC_EVAL VERNAC_ELABORATE VERNAC_LOAD
-%token VERNAC_DEFINITION VERNAC_INDUCTIVE  
+%token VERNAC_DEFINITION VERNAC_FIXPOINT VERNAC_INDUCTIVE  
 %token VERNAC_SET VERNAC_FLAG_VARIANT VERNAC_FLAG_FUEL 
 %token VERNAC_VARIANT_G VERNAC_VARIANT_S VERNAC_VARIANT_N
 %token VERNAC_SEPARATOR
@@ -112,12 +120,18 @@ command :
 // Definition foo (x : Type1) : Type1 := ...
 | VERNAC_DEFINITION; id=id; args=args0; COLON; ty=term; ASSIGN ; body=top  
  { mk_definition id args ty body }
+// Fixpoint foo (x : Type1) {struct n} : Type1 := ...
+| VERNAC_FIXPOINT; id=id; args=args0; struct_id=struct_id; COLON; ty=term; ASSIGN ; body=top  
+ { mk_fix id args struct_id ty body }
 // Load "filename"
 | VERNAC_LOAD; filename=FILENAME  { Load filename }
 // Inductive list (a : Type0) : Type0 := <ctor_decls>
 | VERNAC_INDUCTIVE; id=id; params=args0; COLON; ty=term; ASSIGN; ctors=list(ctor_decl)
  { mk_ind_decl id params ty ctors }
 
+%inline struct_id :
+| LBRACE; KWD_STRUCT; id=id; RBRACE { id }
+
 ctor_decl :
 | VBAR; id=id; args=args0; COLON; ty=term { (id, args, ty) }
 
diff --git a/lib/parsing/parserMessages.messages b/lib/parsing/parserMessages.messages
index 8f7566b..e3efd65 100644
--- a/lib/parsing/parserMessages.messages
+++ b/lib/parsing/parserMessages.messages
@@ -14,7 +14,7 @@ For example:
 
 term_parser: ID RPAREN
 ##
-## Ends in an error in state: 130.
+## Ends in an error in state: 141.
 ##
 ## term_parser -> top . EOF [ # ]
 ## top -> top . COLON term [ EOF COLON ]
@@ -91,7 +91,7 @@ term_parser: KWD_LAMBDA LPAREN ID COLON ID KWD_LET
 ##
 ## Ends in an error in state: 36.
 ##
-## arg -> LPAREN nonempty_list(id) COLON term . RPAREN [ LPAREN COMMA COLON BIG_ARROW ]
+## arg -> LPAREN nonempty_list(id) COLON term . RPAREN [ LPAREN LBRACE COMMA COLON BIG_ARROW ]
 ##
 ## The known suffix of the stack is as follows:
 ## LPAREN nonempty_list(id) COLON term
@@ -143,7 +143,7 @@ term_parser: KWD_LAMBDA LPAREN ID COLON RPAREN
 ##
 ## Ends in an error in state: 23.
 ##
-## arg -> LPAREN nonempty_list(id) COLON . term RPAREN [ LPAREN COMMA COLON BIG_ARROW ]
+## arg -> LPAREN nonempty_list(id) COLON . term RPAREN [ LPAREN LBRACE COMMA COLON BIG_ARROW ]
 ##
 ## The known suffix of the stack is as follows:
 ## LPAREN nonempty_list(id) COLON
@@ -175,7 +175,7 @@ term_parser: KWD_LAMBDA LPAREN RPAREN
 ##
 ## Ends in an error in state: 21.
 ##
-## arg -> LPAREN . nonempty_list(id) COLON term RPAREN [ LPAREN COMMA COLON BIG_ARROW ]
+## arg -> LPAREN . nonempty_list(id) COLON term RPAREN [ LPAREN LBRACE COMMA COLON BIG_ARROW ]
 ##
 ## The known suffix of the stack is as follows:
 ## LPAREN
@@ -373,7 +373,7 @@ For example:
 
 term_parser: RPAREN
 ##
-## Ends in an error in state: 129.
+## Ends in an error in state: 140.
 ##
 ## term_parser' -> . term_parser [ # ]
 ##
@@ -389,7 +389,7 @@ For example:
 
 program_parser: RPAREN
 ##
-## Ends in an error in state: 123.
+## Ends in an error in state: 134.
 ##
 ## program_parser' -> . program_parser [ # ]
 ##
@@ -406,7 +406,7 @@ For example:
 
 program_parser: VERNAC_EVAL VERNAC_SEPARATOR
 ##
-## Ends in an error in state: 97.
+## Ends in an error in state: 108.
 ##
 ## command -> VERNAC_EVAL . top [ VERNAC_SEPARATOR ]
 ##
@@ -445,7 +445,7 @@ For example:
 
 program_parser: VERNAC_ELABORATE VERNAC_SEPARATOR
 ##
-## Ends in an error in state: 99.
+## Ends in an error in state: 110.
 ##
 ## command -> VERNAC_ELABORATE . top [ VERNAC_SEPARATOR ]
 ##
@@ -459,7 +459,7 @@ For example:
 
 program_parser: VERNAC_CHECK VERNAC_SEPARATOR
 ##
-## Ends in an error in state: 108.
+## Ends in an error in state: 119.
 ##
 ## command -> VERNAC_CHECK . top [ VERNAC_SEPARATOR ]
 ##
@@ -473,7 +473,7 @@ For example:
 
 program_parser: VERNAC_ELABORATE ID VERNAC_SEPARATOR VERNAC_SEPARATOR
 ##
-## Ends in an error in state: 124.
+## Ends in an error in state: 135.
 ##
 ## list(sequenced_command) -> sequenced_command . list(sequenced_command) [ EOF ]
 ##
@@ -536,7 +536,7 @@ For example:
 
 program_parser: VERNAC_CHECK ID RPAREN
 ##
-## Ends in an error in state: 109.
+## Ends in an error in state: 120.
 ##
 ## command -> VERNAC_CHECK top . [ VERNAC_SEPARATOR ]
 ## top -> top . COLON term [ VERNAC_SEPARATOR COLON ]
@@ -553,7 +553,7 @@ program_parser: VERNAC_CHECK ID RPAREN
 ##
 program_parser: VERNAC_ELABORATE ID VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 100.
+## Ends in an error in state: 111.
 ##
 ## command -> VERNAC_ELABORATE top . [ VERNAC_SEPARATOR ]
 ## top -> top . COLON term [ VERNAC_SEPARATOR COLON ]
@@ -570,7 +570,7 @@ program_parser: VERNAC_ELABORATE ID VERNAC_VARIANT_S
 ##
 program_parser: VERNAC_EVAL ID VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 98.
+## Ends in an error in state: 109.
 ##
 ## command -> VERNAC_EVAL top . [ VERNAC_SEPARATOR ]
 ## top -> top . COLON term [ VERNAC_SEPARATOR COLON ]
@@ -593,7 +593,7 @@ For example:
 
 program_parser: VERNAC_DEFINITION VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 101.
+## Ends in an error in state: 112.
 ##
 ## command -> VERNAC_DEFINITION . id list(arg) COLON term ASSIGN top [ VERNAC_SEPARATOR ]
 ##
@@ -607,7 +607,7 @@ For example:
 
 program_parser: VERNAC_DEFINITION ID VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 102.
+## Ends in an error in state: 113.
 ##
 ## command -> VERNAC_DEFINITION id . list(arg) COLON term ASSIGN top [ VERNAC_SEPARATOR ]
 ##
@@ -625,7 +625,7 @@ command_parser: VERNAC_DEFINITION ID LPAREN ID COLON ID RPAREN VERNAC_VARIANT_S
 ##
 ## Ends in an error in state: 92.
 ##
-## list(arg) -> arg . list(arg) [ COLON ]
+## list(arg) -> arg . list(arg) [ LBRACE COLON ]
 ##
 ## The known suffix of the stack is as follows:
 ## arg
@@ -640,7 +640,7 @@ For example:
 
 program_parser: VERNAC_DEFINITION ID COLON VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 104.
+## Ends in an error in state: 115.
 ##
 ## command -> VERNAC_DEFINITION id list(arg) COLON . term ASSIGN top [ VERNAC_SEPARATOR ]
 ##
@@ -654,7 +654,7 @@ For example:
 
 program_parser: VERNAC_DEFINITION ID COLON ID VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 105.
+## Ends in an error in state: 116.
 ##
 ## command -> VERNAC_DEFINITION id list(arg) COLON term . ASSIGN top [ VERNAC_SEPARATOR ]
 ##
@@ -674,7 +674,7 @@ For example:
 
 command_parser: VERNAC_DEFINITION ID COLON ID ASSIGN VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 106.
+## Ends in an error in state: 117.
 ##
 ## command -> VERNAC_DEFINITION id list(arg) COLON term ASSIGN . top [ VERNAC_SEPARATOR ]
 ##
@@ -688,7 +688,7 @@ For example:
 
 command_parser: VERNAC_DEFINITION ID COLON ID ASSIGN ID VBAR
 ##
-## Ends in an error in state: 107.
+## Ends in an error in state: 118.
 ##
 ## command -> VERNAC_DEFINITION id list(arg) COLON term ASSIGN top . [ VERNAC_SEPARATOR ]
 ## top -> top . COLON term [ VERNAC_SEPARATOR COLON ]
@@ -740,7 +740,7 @@ For example:
 
 command_parser: VERNAC_CHECK ID VERNAC_SEPARATOR VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 110.
+## Ends in an error in state: 121.
 ##
 ## command_parser -> sequenced_command . EOF [ # ]
 ##
@@ -785,9 +785,9 @@ For example:
 
 command_parser: VERNAC_SET VERNAC_FLAG_FUEL INT VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 113.
+## Ends in an error in state: 124.
 ##
-## sequenced_command -> command . VERNAC_SEPARATOR [ VERNAC_SET VERNAC_LOAD VERNAC_INDUCTIVE VERNAC_EVAL VERNAC_ELABORATE VERNAC_DEFINITION VERNAC_CHECK EOF ]
+## sequenced_command -> command . VERNAC_SEPARATOR [ VERNAC_SET VERNAC_LOAD VERNAC_INDUCTIVE VERNAC_FIXPOINT VERNAC_EVAL VERNAC_ELABORATE VERNAC_DEFINITION VERNAC_CHECK EOF ]
 ##
 ## The known suffix of the stack is as follows:
 ## command
@@ -799,7 +799,7 @@ For example:
 
 flag_parser: VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 119.
+## Ends in an error in state: 130.
 ##
 ## flag_parser' -> . flag_parser [ # ]
 ##
@@ -814,7 +814,7 @@ For example:
 
 flag_parser: VERNAC_FLAG_FUEL INT VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 121.
+## Ends in an error in state: 132.
 ##
 ## flag_parser -> flag . EOF [ # ]
 ##
@@ -935,7 +935,7 @@ For example:
 
 ctor_decl_parser: VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 115.
+## Ends in an error in state: 126.
 ##
 ## ctor_decl_parser' -> . ctor_decl_parser [ # ]
 ##
@@ -994,7 +994,7 @@ For example:
 
 ctor_decl_parser: VBAR ID COLON ID VERNAC_VARIANT_S
 ##
-## Ends in an error in state: 117.
+## Ends in an error in state: 128.
 ##
 ## ctor_decl_parser -> ctor_decl . EOF [ # ]
 ##
@@ -1339,4 +1339,217 @@ branch_parser: VBAR ID BIG_ARROW ID VBAR
 ##
 
 I'm currently parsing a branch of a match expression.
-After `$0`, the end of file is expected.
\ No newline at end of file
+After `$0`, the end of file is expected.
+
+
+
+
+command_parser: VERNAC_INDUCTIVE ID LPAREN ID COLON ID RPAREN LBRACE
+##
+## Ends in an error in state: 83.
+##
+## command -> VERNAC_INDUCTIVE id list(arg) . COLON term ASSIGN list(ctor_decl) [ VERNAC_SEPARATOR ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_INDUCTIVE id list(arg)
+##
+## WARNING: This example involves spurious reductions.
+## This implies that, although the LR(1) items shown above provide an
+## accurate view of the past (what has been recognized so far), they
+## may provide an INCOMPLETE view of the future (what was expected next).
+## In state 92, spurious reduction of production list(arg) ->
+## In state 93, spurious reduction of production list(arg) -> arg list(arg)
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+ctor_decl_parser: VBAR ID LPAREN ID COLON ID RPAREN LBRACE
+##
+## Ends in an error in state: 89.
+##
+## ctor_decl -> VBAR id list(arg) . COLON term [ VERNAC_SEPARATOR VBAR EOF ]
+##
+## The known suffix of the stack is as follows:
+## VBAR id list(arg)
+##
+## WARNING: This example involves spurious reductions.
+## This implies that, although the LR(1) items shown above provide an
+## accurate view of the past (what has been recognized so far), they
+## may provide an INCOMPLETE view of the future (what was expected next).
+## In state 92, spurious reduction of production list(arg) ->
+## In state 93, spurious reduction of production list(arg) -> arg list(arg)
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+command_parser: VERNAC_FIXPOINT VERNAC_VARIANT_S
+##
+## Ends in an error in state: 97.
+##
+## command -> VERNAC_FIXPOINT . id list(arg) LBRACE KWD_STRUCT id RBRACE COLON term ASSIGN top [ VERNAC_SEPARATOR ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_FIXPOINT
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+command_parser: VERNAC_FIXPOINT ID VERNAC_VARIANT_S
+##
+## Ends in an error in state: 98.
+##
+## command -> VERNAC_FIXPOINT id . list(arg) LBRACE KWD_STRUCT id RBRACE COLON term ASSIGN top [ VERNAC_SEPARATOR ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_FIXPOINT id
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+command_parser: VERNAC_FIXPOINT ID LPAREN ID COLON ID RPAREN COLON
+##
+## Ends in an error in state: 99.
+##
+## command -> VERNAC_FIXPOINT id list(arg) . LBRACE KWD_STRUCT id RBRACE COLON term ASSIGN top [ VERNAC_SEPARATOR ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_FIXPOINT id list(arg)
+##
+## WARNING: This example involves spurious reductions.
+## This implies that, although the LR(1) items shown above provide an
+## accurate view of the past (what has been recognized so far), they
+## may provide an INCOMPLETE view of the future (what was expected next).
+## In state 92, spurious reduction of production list(arg) ->
+## In state 93, spurious reduction of production list(arg) -> arg list(arg)
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+command_parser: VERNAC_FIXPOINT ID LBRACE VERNAC_VARIANT_S
+##
+## Ends in an error in state: 100.
+##
+## command -> VERNAC_FIXPOINT id list(arg) LBRACE . KWD_STRUCT id RBRACE COLON term ASSIGN top [ VERNAC_SEPARATOR ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_FIXPOINT id list(arg) LBRACE
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+command_parser: VERNAC_FIXPOINT ID LBRACE KWD_STRUCT VERNAC_VARIANT_S
+##
+## Ends in an error in state: 101.
+##
+## command -> VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT . id RBRACE COLON term ASSIGN top [ VERNAC_SEPARATOR ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+command_parser: VERNAC_FIXPOINT ID LBRACE KWD_STRUCT ID VERNAC_VARIANT_S
+##
+## Ends in an error in state: 102.
+##
+## command -> VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT id . RBRACE COLON term ASSIGN top [ VERNAC_SEPARATOR ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT id
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+command_parser: VERNAC_FIXPOINT ID LBRACE KWD_STRUCT ID RBRACE VERNAC_VARIANT_S
+##
+## Ends in an error in state: 103.
+##
+## command -> VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT id RBRACE . COLON term ASSIGN top [ VERNAC_SEPARATOR ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT id RBRACE
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+command_parser: VERNAC_FIXPOINT ID LBRACE KWD_STRUCT ID RBRACE COLON VERNAC_VARIANT_S
+##
+## Ends in an error in state: 104.
+##
+## command -> VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT id RBRACE COLON . term ASSIGN top [ VERNAC_SEPARATOR ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT id RBRACE COLON
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+command_parser: VERNAC_FIXPOINT ID LBRACE KWD_STRUCT ID RBRACE COLON ID VERNAC_SEPARATOR
+##
+## Ends in an error in state: 105.
+##
+## command -> VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT id RBRACE COLON term . ASSIGN top [ VERNAC_SEPARATOR ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT id RBRACE COLON term
+##
+## WARNING: This example involves spurious reductions.
+## This implies that, although the LR(1) items shown above provide an
+## accurate view of the past (what has been recognized so far), they
+## may provide an INCOMPLETE view of the future (what was expected next).
+## In state 29, spurious reduction of production term -> fact
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+command_parser: VERNAC_FIXPOINT ID LBRACE KWD_STRUCT ID RBRACE COLON ID ASSIGN VERNAC_VARIANT_S
+##
+## Ends in an error in state: 106.
+##
+## command -> VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT id RBRACE COLON term ASSIGN . top [ VERNAC_SEPARATOR ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT id RBRACE COLON term ASSIGN
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+command_parser: VERNAC_FIXPOINT ID LBRACE KWD_STRUCT ID RBRACE COLON ID ASSIGN ID VBAR
+##
+## Ends in an error in state: 107.
+##
+## command -> VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT id RBRACE COLON term ASSIGN top . [ VERNAC_SEPARATOR ]
+## top -> top . COLON term [ VERNAC_SEPARATOR COLON ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_FIXPOINT id list(arg) LBRACE KWD_STRUCT id RBRACE COLON term ASSIGN top
+##
+## WARNING: This example involves spurious reductions.
+## This implies that, although the LR(1) items shown above provide an
+## accurate view of the past (what has been recognized so far), they
+## may provide an INCOMPLETE view of the future (what was expected next).
+## In state 29, spurious reduction of production term -> fact
+## In state 60, spurious reduction of production top -> term
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
+
+command_parser: VERNAC_DEFINITION ID LPAREN ID COLON ID RPAREN LBRACE
+##
+## Ends in an error in state: 114.
+##
+## command -> VERNAC_DEFINITION id list(arg) . COLON term ASSIGN top [ VERNAC_SEPARATOR ]
+##
+## The known suffix of the stack is as follows:
+## VERNAC_DEFINITION id list(arg)
+##
+## WARNING: This example involves spurious reductions.
+## This implies that, although the LR(1) items shown above provide an
+## accurate view of the past (what has been recognized so far), they
+## may provide an INCOMPLETE view of the future (what was expected next).
+## In state 92, spurious reduction of production list(arg) ->
+## In state 93, spurious reduction of production list(arg) -> arg list(arg)
+##
+
+<YOUR SYNTAX ERROR MESSAGE HERE>
diff --git a/lib/reduction/cast_CIC.ml b/lib/reduction/cast_CIC.ml
index 3bd7c90..317f4ab 100644
--- a/lib/reduction/cast_CIC.ml
+++ b/lib/reduction/cast_CIC.ml
@@ -93,9 +93,24 @@ module Make (ST : Store) : CastCICRed = struct
     | Ok (HInductive i), Ok (HInductive j) -> i = j
     | _, _ -> assert false
 
+  let rec is_fix_neutral (t : term) : bool =
+    let rec get_args acc = function
+      | Fixpoint fi -> Ok (fi.fix_rarg, List.rev acc)
+      | App (t, u) -> get_args (u :: acc) t
+      | _ -> Error ()
+    in
+    let res =
+      let* narg, args = get_args [] t in
+      match List.nth_opt args narg with
+      | None -> Ok true
+      | Some t -> Ok (is_neutral t)
+    in
+    Result.fold ~ok:(fun x -> x) ~error:(fun _ -> false) res
+
   (** Checks if a term is in neutral form *)
-  let rec is_neutral : term -> bool = function
+  and is_neutral : term -> bool = function
     | Var _ -> true
+    | t when is_fix_neutral t -> true
     | App (t, _)
     | Unknown t
     | Err t
@@ -115,15 +130,35 @@ module Make (ST : Store) : CastCICRed = struct
     | Universe _ | Unknown (Universe _) | Err (Universe _) | Inductive _ -> true
     | _ -> is_neutral term
 
+  let is_fix_canonical term : bool =
+    let rec get_args acc = function
+      | Fixpoint fi -> Ok (fi.fix_rarg, acc)
+      | App (t, _) -> get_args (acc + 1) t
+      | _ -> Error ()
+    in
+    Result.fold
+      ~ok:(fun (rarg, nargs) -> nargs <= rarg)
+      ~error:(fun _ -> false)
+      (get_args 0 term)
+
   (** Checks if a term is in canonical form *)
   let is_canonical : term -> bool = function
-    | Universe _ | Lambda _ | Prod _ | Constructor _ | Inductive _ -> true
+    | Universe _ | Lambda _ | Prod _ | Constructor _ | Inductive _ | Fixpoint _ -> true
     | Unknown t -> is_unknown_or_error_canonical t
     | Err t -> is_unknown_or_error_canonical t
     | Cast { source = ty; target = Unknown (Universe i); term = _ } when is_germ i ty ->
       true
+    | t when is_fix_canonical t -> true
     | t -> is_neutral t
 
+  (** Unfolds one recursion step of a Fixpoint *)
+  let unfold_fixpoint (fi : fix_info) : int * term =
+    fi.fix_rarg, subst1 fi.fix_id (Fixpoint fi) fi.fix_body
+
+  let is_valid_fix_arg : term -> bool = function
+    | Constructor _ | Unknown _ | Err _ -> true
+    | _ -> false
+
   (** The representation of a continuation of the CEK machine *)
   type continuation =
     (* Reducing the lhs of an application *)
@@ -141,6 +176,7 @@ module Make (ST : Store) : CastCICRed = struct
     (* Reducing the discriminee of a match. The inductive's name, the z variable, 
    the predicate and the f variable are stored in the state. *)
     | KMatch_discr of (Name.t * Name.t * term * Name.t * branch list)
+    | KFix_app of fix_info * term list
 
   (* Type alias *)
   type state = term * continuation list
@@ -185,6 +221,10 @@ module Make (ST : Store) : CastCICRed = struct
     (* Match-Err *)
     | Match { discr = Err (Inductive _) as discr; z; pred; _ }, _ ->
       Err (subst1 z discr pred), cont
+    (* Fixpoint unfold *)
+    | term, KFix_app (fi, args) :: cont when is_valid_fix_arg term ->
+      let _, fn = unfold_fixpoint fi in
+      List.fold_left (fun t u -> App (t, u)) fn (List.rev (term :: args)), cont
     (* Ind-Unk *)
     | ( Cast
           { source = Inductive (ind1, i1, _)
@@ -263,7 +303,7 @@ module Make (ST : Store) : CastCICRed = struct
       let casted_args, _ =
         List.fold_left cast_arg ([], target_args) (List.combine source_args ci.args)
       in
-      Constructor { ci with params = target_params; args = casted_args }, cont
+      Constructor { ci with params = target_params; args = List.rev casted_args }, cont
       (* Head-Err *)
     | Cast { source; target; term = _ }, _
       when is_type source && is_type target && not (equal_head source target) ->
@@ -323,6 +363,8 @@ module Make (ST : Store) : CastCICRed = struct
       term, KCast_term (source, target) :: cont
     | term, KCast_term (source, target) :: cont when is_canonical term ->
       Cast { source; target; term }, cont
+    | term, KFix_app (fi, args) :: cont when is_canonical term ->
+      List.fold_left (fun t u -> App (t, u)) (Fixpoint fi) (List.rev (term :: args)), cont
     | discr, KMatch_discr (ind, z, pred, f, branches) :: cont when is_canonical discr ->
       Match { ind; discr; z; pred; f; branches }, cont
     | App (t, u), _ -> t, KApp_l u :: cont
@@ -331,6 +373,20 @@ module Make (ST : Store) : CastCICRed = struct
     | Cast { source; target; term }, _ -> target, KCast_target (source, term) :: cont
     | Match { ind; discr; z; pred; f; branches }, _ ->
       discr, KMatch_discr (ind, z, pred, f, branches) :: cont
+    | Fixpoint fi, cont ->
+      let rec get_args acc n cont =
+        match n, cont with
+        | 0, _ -> Some (acc, cont)
+        | n, KApp_l u :: ks -> get_args (u :: acc) (n - 1) ks
+        | _, _ -> None
+      in
+      let args = get_args [] (fi.fix_rarg + 1) cont in
+      (match args with
+      | Some (c :: args, cont) -> c, KFix_app (fi, args) :: cont
+      | _ -> assert false)
+    | _, KFix_app _ :: _ ->
+      print_endline (to_string term);
+      raise (Stuck_term term)
     | _, _ -> raise (Stuck_term term)
 
   (** Transitive clousure of reduce1 with fuel *)
@@ -361,6 +417,8 @@ module Make (ST : Store) : CastCICRed = struct
       | KCast_term (source, target) -> Cast { source; target; term }
       | KMatch_discr (ind, z, pred, f, branches) ->
         Match { ind; discr = term; z; pred; f; branches }
+      | KFix_app (fi, args) ->
+        List.fold_left (fun t u -> App (t, u)) (Fixpoint fi) (List.rev args)
     in
     List.fold_left fill_hole1 term
 
diff --git a/lib/typing/cast_CIC.ml b/lib/typing/cast_CIC.ml
index 64230fa..4143df5 100644
--- a/lib/typing/cast_CIC.ml
+++ b/lib/typing/cast_CIC.ml
@@ -10,6 +10,7 @@ type type_error =
   | `Err_not_product of term * term
   | `Err_not_universe of term * term
   | `Err_not_inductive of term * term
+  | `Err_invalid_fixpoint of fix_info
   ]
 
 type reduction_error =
@@ -33,6 +34,7 @@ let string_of_error = function
   | `Err_not_enough_fuel -> "not enough fuel"
   | `Err_stuck_term _term -> "stuck term"
   | `Err_free_const -> "free constant"
+  | `Err_invalid_fixpoint _fi -> "invalid fixpoint"
 
 module type Reducer = sig
   val reduce : term -> (term, errors) result
@@ -61,6 +63,14 @@ module Make (ST : Store) (R : Reducer) : CastCICTyping = struct
   type i = (term, errors) result
   type c = (unit, errors) result
 
+  let fix_guard _term = Ok ()
+
+  let fix_context (fi : fix_info) : typing_context =
+    Name.Map.singleton fi.fix_id fi.fix_type
+
+  let wf_fixpoint (fi : fix_info) =
+    if is_lambda fi.fix_body then Ok () else Error (`Err_invalid_fixpoint fi)
+
   let are_convertible t1 t2 : (unit, [> type_error ]) result =
     let* v1 = R.reduce t1 in
     let* v2 = R.reduce t2 in
@@ -121,6 +131,13 @@ module Make (ST : Store) (R : Reducer) : CastCICTyping = struct
       let branch_ctx = Name.Map.add f (Prod { id = z; dom = indt; body = pred }) ctx in
       let* _ = map_results (check_branch branch_ctx z pred params level) branches in
       Ok (subst1 z discr pred)
+    | Fixpoint fi ->
+      let fix_ctx = Name.Map.union (fun _ x _ -> Some x) (fix_context fi) ctx in
+      let* () = fix_guard fi.fix_body in
+      let* () = wf_fixpoint fi in
+      let* _ = infer_univ ctx fi.fix_type in
+      let* () = check_type fix_ctx fi.fix_body fi.fix_type in
+      Ok fi.fix_type
 
   and check_type (ctx : typing_context) (t : term) (ty : term)
       : (unit, [> type_error ]) result
diff --git a/lib/typing/cast_CIC.mli b/lib/typing/cast_CIC.mli
index 9f9ff0b..36fb01d 100644
--- a/lib/typing/cast_CIC.mli
+++ b/lib/typing/cast_CIC.mli
@@ -7,6 +7,7 @@ type type_error =
   | `Err_not_product of term * term
   | `Err_not_universe of term * term
   | `Err_not_inductive of term * term
+  | `Err_invalid_fixpoint of fix_info
   ]
 
 type reduction_error =
diff --git a/test/parser/testable.ml b/test/parser/testable.ml
index d1f5529..310112e 100644
--- a/test/parser/testable.ml
+++ b/test/parser/testable.ml
@@ -17,6 +17,7 @@ let command =
     | Elab t -> "elab " ^ to_string t
     | Set flag -> "set " ^ Config.Flag.to_string flag
     | Define gdef -> "definition " ^ def_to_string gdef
+    | Fix (_, gdef) -> "fixpoint " ^ def_to_string gdef
     | Load filename -> Format.asprintf "import \"%s\"" filename
     | Inductive (ind, _ctors) ->
       Format.asprintf "inductive %s" (Common.Id.Name.to_string ind.name)