| Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
| Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
let curi,metasenv,pbo,pty = proof in
| Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
| Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
let curi,metasenv,pbo,pty = proof in