fact: Fixpoint count (A:Type)(t:ntree A){struct t} : Z := match t with | nnode _ a l => 1 + count_list A l end with count_list (A:Type)(l:nforest A){struct l} : Z := match l with | nnil _ => 0 | ncons _ t tl => count A t + count_list A tl end.
imports: ZArith List Arith Zwf Relations Inverse_Image