refine ⟨r₁, rfl, h⟩
μ : Sort ?u.98034
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr✝ : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
k : ℕ
injr : Function.Injective Φ.rel
r₁ : L₁.Rel k
v : Fin k → M
h : rel r₁ v
⊢ ∃ r₁_1, Φ.rel r₁_1 = Φ.rel r₁ ∧ rel r₁_1 v
no goals