induction q using Superintuitionistic.Formula.rec' generalizing v with
| hatom a =>
  constructor;
  . intro _ _ h;
    simp_all only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies];
    exact iV_hereditary h (by assumption);
  . intro h;
    simpa only [Satisfies.iff_models, Satisfies, Formula.Kripke.Satisfies] using h v $ iF.Rel_refl v;
| _ => simp_all;
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q✝ r : Superintuitionistic.Formula α
h✝ : ¬𝐈𝐧𝐭 ⊢! p
iF : Superintuitionistic.Kripke.Frame' α
left✝ : iF ∈ 𝔽(𝗘𝗙𝗤)
iV : Superintuitionistic.Kripke.Valuation iF.World α
iV_hereditary : ∀ {w₁ w₂ : iF.World}, w₁ ≺ w₂ → ∀ {a : α}, iV w₁ a → iV w₂ a
w : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
h : ¬Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } w p
M : Kripke.Model α := { Frame := { World := iF.World, World_nonempty := ⋯, Rel := iF.Rel }, Valuation := iV }
q : Superintuitionistic.Formula α
v : { Frame := iF, Valuation := iV, hereditary := ⋯ }.World
⊢ Satisfies { Frame := iF, Valuation := iV, hereditary := ⋯ } v q ↔ Formula.Kripke.Satisfies M v (qᵍ)
no goals