cases i using Fin.cases <;> simp [Fin.eq_zero]
case h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
i : Fin 2
⊢ Semiterm.lMap Language.oringEmb (v i) =
    ![Semiterm.lMap Language.oringEmb (v 0), Semiterm.lMap Language.oringEmb (v 1)] i
no goals