proposition: Lemma zigzag_unfold : forall b, zigzag b = if b then LBin b LLeaf (zigzag false) else LBin b (zigzag true) LLeaf.
proof: Proof. intro b;LTree_unfold (zigzag b); cbn ; case b; simpl; auto. Qed.
imports: Ltree building graft