have : T ⊢ p := System.Subtheory.prf (System.byAxm hp)
L : Language
T U : Theory L
inst✝² : U ≼ T
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Nonempty M
hM : M ⊧ₘ* T
p : Sentence L
hp : p ∈ U
⊢ inst✝¹.toStruc ⊧ p
L : Language
T U : Theory L
inst✝² : U ≼ T
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Nonempty M
hM : M ⊧ₘ* T
p : Sentence L
hp : p ∈ U
this : T ⊢ p
⊢ inst✝¹.toStruc ⊧ p