Goal:
    A : Type  B : Type  empty : B  node : tree A -> option A -> tree A -> B
  ============================
   (forall (l : tree A) (o : option A) (r : tree A),
    not_trivially_empty l o r -> tree_case (Node l o r) = node l o r)


DEBUG:Going to execute:
destruct l, o, r; simpl; intros