letI := Classical.typeDecidableEq
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
⊢ T ⊢! σ
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
⊢ T ⊢! σ