Goal:
  
  A : Type
  i : positive
  IHi : forall (j : positive) (m : tree' A),
        i <> j -> get i (rem' j m) = get' i m
  j : positive
  m1 : tree' A
  m2 : tree' A
  H : xI i <> xO j
  ============================
   (get i (Nodes m2) = get' i m2)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3

Goals:

DEBUG:Going to execute:
apply IHi

Goals:

DEBUG:Going to execute:
congruence

Goals:

DEBUG:Going to execute:
<coq-core.plugins.cc::cc@0> $1