exact ⟨v 0, H 0, v 1, H 1, by intro i; cases i using Fin.cases <;> simp [Fin.eq_zero]⟩
case pos.mp
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
H : ∀ (a : Fin 2), ω (v a) = ![t, u] a
⊢ ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ ∀ (a : Fin 2), v a = ![t', x] a
no goals