exact mapl_inj (b := 0 :> Fin.succ ∘ b)
(Matrix.injective_vecCons ((Fin.succ_injective _).comp hb) (fun _ => (Fin.succ_ne_zero _).symm)) hf h
case hex
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝² x✝¹ : ℕ
ξ✝ : Type u_5
x✝ : Type u_6
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
h : (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝
⊢ p = p✝
no goals