| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition