- term:Cic.term -> ?subst:Cic.substitution -> ProofEngineTypes.proof * int ->
- Cic.substitution * (ProofEngineTypes.proof * int list)
+ term:Cic.term -> ?subst:Cic.substitution -> ?maxmeta:int -> ProofEngineTypes.proof * int ->
+ Cic.substitution * (ProofEngineTypes.proof * int list) * int