-let destroy_nat annterm =
- let is_zero = function
- | Cic.AMutConstruct (_, uri, 0, 1, _) when Obj.is_nat_URI uri -> true
- | _ -> false
- in
- let is_succ = function
- | Cic.AMutConstruct (_, uri, 0, 2, _) when Obj.is_nat_URI uri -> true
- | _ -> false
- in
- let rec aux acc = function
- | Cic.AAppl (_, [he ; tl]) when is_succ he -> aux (acc + 1) tl
- | t when is_zero t -> Some acc
- | _ -> None in
- aux 0 annterm
-