let paramodulation_ok =
match paramodulation with
| None -> false
| Some _ ->
let _, metasenv, _, _ = proof in
let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
let paramodulation_ok =
match paramodulation with
| None -> false
| Some _ ->
let _, metasenv, _, _ = proof in
let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in