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


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