- let subproofs,args = aux l1 in
- if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then
+ let need_lifting =
+ test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts in
+ let subproofs,args = aux (n + if need_lifting then 1 else 0) l1 in
+ if need_lifting then