proposition: Lemma treeincr_fix : forall t, treeincr t = Treeincr treeincr t.
proof: Proof. Proof using. applys (FixFun_fix subtree). reflexivity. apply subtree_wf. introv H. unfold Treeincr. destruct x. auto. fequals. apply~ map_congr. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat