\import Data.List
\import Paths
\import Paths.Meta

\data Tree : \Set
  | leaf (n : Nat)
  | node (t : List Tree) \with { leaf n :: nil => leaf (suc n) }

\func tsuc (a : Tree) => node (a :: nil)

\func add (a b : Tree): Tree \elim b
  | leaf 0 => a
  | leaf (suc n) => tsuc (add a (leaf n))
  | node nil => node nil
  | node (n :: nil) => tsuc (add a n)
  | node (n :: n' :: ns) => node (add_list a (n :: n' :: ns))
  \where {
    \func add_list (a : Tree) (b : List Tree) : List Tree \elim b
      | nil => nil
      | b :: bs => add a b :: add_list a bs
  }

\func add-assoc {a b c : Tree} : add a (add b c) = add (add a b) c \elim c
  | leaf 0 => idp
  | leaf (suc n) => pmap tsuc add-assoc
  | node nil => idp
  | node (n :: nil) => pmap tsuc add-assoc
  | node (n :: n' :: ns) => rewrite (add-assoc, add-assoc, add_list-assoc) idp
  \where {
    \func add_list-assoc {a b : Tree} {cs : List Tree}
      : add.add_list a (add.add_list b cs) = add.add_list (add a b) cs \elim cs
      | nil => idp
      | c :: cs => pmap2 (::) add-assoc add_list-assoc
  }