+ let map2 case (_, cty) =
+ let map (h, case, k) premise =
+ if h > 0 then pred h, lift k 1 case, k else
+ if is_recursive premise then 0, lift (succ k) 1 case, succ k else
+ 0, case, succ k
+ in
+ let premises, _ = Cl.split context cty in
+ let _, lifted_case, _ =
+ List.fold_left map (lpsno, case, 1) (List.rev (List.tl premises))
+ in
+ lifted_case
+ in
+ let lifted_cases = List.map2 map2 cases constructors in
+ let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
+ Some (C.AAppl (id, args))
+with Invalid_argument _ -> failwith "PCn.mk_ind"