let (_, context, _) = CicUtil.lookup_meta goal metasenv in
let proof',goal' = aux count context status in
assert (goal = goal') ;
let (_, context, _) = CicUtil.lookup_meta goal metasenv in
let proof',goal' = aux count context status in
assert (goal = goal') ;