+let destroy_nat =
+ let is_nat_URI = NUri.eq (NUri.uri_of_string
+ "cic:/matita/ng/arithmetics/nat/nat.ind") in
+ let is_zero = function
+ | NCic.Const (NReference.Ref (uri, NReference.Con (0, 1, 0))) when
+ is_nat_URI uri -> true
+ | _ -> false
+ in
+ let is_succ = function
+ | NCic.Const (NReference.Ref (uri, NReference.Con (0, 2, 0))) when
+ is_nat_URI uri -> true
+ | _ -> false
+ in
+ let rec aux acc = function
+ | NCic.Appl [he ; tl] when is_succ he -> aux (acc + 1) tl
+ | t when is_zero t -> Some acc
+ | _ -> None
+ in
+ aux 0
+