let metasenv' = List.filter (fun (i,_,_)->i<>goalno) canonical_menv in
let goal = [], metasenv', cleaned_goal in
let env = metasenv,context,CicUniv.empty_ugraph in
let metasenv' = List.filter (fun (i,_,_)->i<>goalno) canonical_menv in
let goal = [], metasenv', cleaned_goal in
let env = metasenv,context,CicUniv.empty_ugraph in