Goal:
  
  ============================
   (forall (A : Type) (i j : positive) (x : A) (m : tree A),
    i <> j -> get i (set j x m) = get i m)


DEBUG:Going to execute:
induction i; destruct j; induction m using tree_ind; intros;
            rewrite set_Empty || rewrite set_Node; 
            rewrite !gNode; auto; try apply IHi