Goal:
    A : Type  i : positive  l : tree A  x : option A  r : tree A
  ============================
   (get i (Node l x r) =
    match i with
    | xI j => get j r
    | xO j => get j l
    | xH => x
    end)


DEBUG:Going to execute:
destruct l, x, r; simpl; auto