Goal:
  
  ============================
   (forall (A : Type) (i : positive) (x : A) (m : tree A),
    get i (set i x m) = Some x)


DEBUG:Going to execute:
induction i; induction m using tree_ind; intros;
            rewrite set_Empty || rewrite set_Node; 
            rewrite gNode