if hj' : j < as.size then
  rewrite [getElem_append_left as bs hj']
  exact has.get_inj i j hi' hj'
else
  rewrite [getElem_append_right as bs (Nat.le_of_not_lt hj')]
  intro hij; exfalso
  exact hdisj _ _ _ _ hij
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
⊢ as[i] = (as ++ bs)[j] → i = j
no goals