induction h using Deduction.inducition! with
| hNec _ ih => exact HilbertBernays₁.D1s (T₀ := T₀) ih;
| hMaxm hp =>
  rcases hp with (hK | hFour)
  . obtain ⟨p, q, e⟩ := hK; subst_vars; apply HilbertBernays₂.D2s (T₀ := T₀);
  . obtain ⟨p, e⟩ := hFour; subst_vars; apply HilbertBernays₃.D3s (T₀ := T₀);
| hLoeb _ ih => exact Loeb.LT T₀ ih;
| hHenkin => simp_all only [Bool.false_eq_true];
| hMdp ihpq ihp =>
  simp [interpretation] at ihpq;
  exact ihpq ⨀ ihp;
| hDne =>
  dsimp [interpretation];
  exact imp_trans! (conj₁'! $ iffComm'! NegationEquiv.negneg_equiv!) dne!;
| _ =>
  dsimp;
  first
  | apply verum!;
  | apply imply₁!;
  | apply imply₂!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
h : 𝐊𝟒(𝐋) ⊢! p
f : realization L α
⊢ T ⊢! f[β] p
no goals