proposition: Lemma len_eq : forall x, len x = S (lmax (map len (sons FB x))).
proof: Proof. intro. unfold len. rewrite Fix_eq. 2: exact len_aux_ext. fold len. unfold len_aux. apply (f_equal (fun l => S (lmax l))). rewrite <- (@pvalues_ith_eq_map A nat). apply pvalues_eq. intros. refl. Qed.
imports: CoLoR(SN ListMax RelUtil ListUtil LogicUtil) Coq(Arith)