let _, metasenv, meta_proof, _ = proof in
let _, context, goal = CicUtil.lookup_meta goal' metasenv in
let equalities, maxm = find_equalities context proof in
let _, metasenv, meta_proof, _ = proof in
let _, context, goal = CicUtil.lookup_meta goal' metasenv in
let equalities, maxm = find_equalities context proof in