{ intro h seq n
  have := h (λ j => if hj : j < (arity (t₁.xor t₂)) then seq ⟨j, hj⟩ else λ _ => false) n
  simp at this
  convert this }
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
⊢ (∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1) →
    ∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i

case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
⊢ (∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i) →
    ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
⊢ (∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i) →
    ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1