let is_conc = function Bv(Conc _), _ -> true | _ -> false