let ((_, metasenv, _, _), metano) = status in
let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
let ((_, metasenv, _, _), metano) = status in
let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in