. intro h t;
  suffices p ∈ t.tableau.1 by exact truthlemma.mpr this;
  exact mem₁_of_provable h;
case mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → CanonicalModel 𝓓 ⊧ p
no goals