let metasenv, ugraph = [], Un.default_ugraph in
let ety = H.get_type "elim_inferred_type" context using in
let _splits, args_no = PEH.split_with_whd (context, ety) in
let metasenv, ugraph = [], Un.default_ugraph in
let ety = H.get_type "elim_inferred_type" context using in
let _splits, args_no = PEH.split_with_whd (context, ety) in