no goals
m n : ℕ
α : Fin (n + 1) → Type u
β : Type v
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (↑(succAbove i) j)
⊢ op i (insertNth i x p i) (insertNth i y q i) = op i x y ∧
    (fun j => op (↑(succAbove i) j) (p j) (q j)) = fun j =>
      op (↑(succAbove i) j) (insertNth i x p (↑(succAbove i) j)) (insertNth i y q (↑(succAbove i) j))
simp