no goals
a₀ a₁ a₂ : Type u
i : ℕ
⊢ lift (#Sequence₂ a₀ a₁ a₂ i) = (#Sequence₂ (ULift a₀) (ULift a₁) (ULift a₂) i)
rcases i with (_ | _ | _ | i) <;>
  simp only [Sequence₂, mk_uLift, mk_fintype, Fintype.card_of_isEmpty, Nat.cast_zero, lift_zero]