induction p using Semiformula.rec' <;>
  simp [*, Semiformula.eval_rel, Semiformula.eval_nrel, Semiterm.valm_uLift, Matrix.comp_vecCons']
L : Language
M : Type v
inst✝ : Structure L M
n : ℕ
ξ : Type u_1
e : Fin n → ULift.{v', v} M
ε : ξ → ULift.{v', v} M
p : Semiformula L ξ n
⊢ (Evalm (ULift.{v', v} M) e ε) p ↔ (Evalm M (fun i => (e i).down) fun i => (ε i).down) p
no goals