Local Contexts, Appendix: Comparing Five Theories of Presupposition Projection

theorem theorem1 (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    (TranspI I C F ↔ dyn I F C ≠ none) ∧
    (∀ D, dyn I F C = some D → ∀ w, D w ↔ (C w ∧ ev I F w = true)) := by
  refine ⟨?_, (dyn_iff I F C).2⟩
  have h1 := (dyn_iff I F C).1
  have : dyn I F C ≠ none ↔ (dyn I F C).isSome = true := by
    cases dyn I F C <;> simp
  rw [this, h1]
  constructor
  · intro H t ht
    exact (local_iff I C t.1 t.2.1).mp (H t ht)
  · intro H t ht
    exact (local_iff I C t.1 t.2.1).mpr (H t ht)

theorem transNo_iff {n : Nat} (P Q : Pred n) : transNo P Q ↔ dynDefined P Q := by
  constructor
  · intro H d hP
    refine Classical.byContradiction (fun hQ => ?_)
    have hQ' : Q d = false := by simpa using hQ
    have h := H (fun e => decide (e = d))
    have h1 : quant fNo P (fun e => Q e && decide (e = d)) = true := by
      rw [quantNo_iff]; intro e ⟨_, h2⟩
      simp at h2; obtain ⟨h3, h4⟩ := h2; subst h4; simp [hQ'] at h3
    rw [h1] at h
    have := (quantNo_iff P (fun e => decide (e = d))).mp h.symm d
    simp [hP] at this
  · intro H γ
    have : (fun d => P d && !(Q d && γ d)) = (fun d => P d && !γ d) := by
      funext d; by_cases hP : P d = true
      · simp [hP, H d hP]
      · simp [hP]
    have h2 : (fun d => P d && (Q d && γ d)) = (fun d => P d && γ d) := by
      funext d; by_cases hP : P d = true
      · simp [hP, H d hP]
      · simp [hP]
    simp only [quant, this, h2]

/-- Lemma 1 (corrected proof): in the propositional fragment the local context exists. -/
theorem lemma1 {Envs : Env W Unit → Prop} (hE : ∀ Ψ, Envs Ψ → Ext Ψ) (C : W → Prop) :
    IsLC Envs C (lc1 Envs C) :=
  ⟨lemma1_step1 hE C, lemma1_step2 hE C⟩

/-- Lemma 1 / Existence theorem 16(a): local contexts exist in the propositional fragment. -/
theorem lc_exists_prop_i (I : Nat → W → Bool) (K : List Frame) (C : W → Prop) :
    ∃ x, LC.IsLC (EnvI I K) C x := ⟨_, LC.lemma1 (envI_ext I K) C⟩

theorem lc_exists_prop_s (I : Nat → W → Bool) (K : List Frame) (C : W → Prop) :
    ∃ x, LC.IsLC (EnvS I K) C x := ⟨_, LC.lemma1 (envS_ext I K) C⟩

theorem lemma1_paper_candidate_fails :
    ∃ (Envs : Env Unit Unit → Prop) (C : Unit → Prop),
      (∀ Ψ, Envs Ψ → Ext Ψ) ∧ Tr Envs C bot ∧ ¬ le (lc1Paper Envs) bot := by
  refine ⟨fun Ψ => Ψ = (fun x w => x w ()), fun _ => False, ?_, ?_, ?_⟩
  · intro Ψ hΨ x y w h; subst hΨ; simp [h]
  · intro Ψ _ γ w hw; exact absurd hw id
  · intro h
    have hp : lc1Paper (fun Ψ : Env Unit Unit => Ψ = (fun x w => x w ())) () () = true := by
      simp only [lc1Paper, decide_eq_true_eq]
      refine ⟨(fun (x : Val Unit Unit) (w : Unit) => x w ()), rfl, top, ?_⟩
      simp [meet, bot, top]
    have := h () () hp
    simp [bot] at this

theorem lemma2 {Envs : Env W D → Prop} {C : W → Prop} {x y : Val W D}
    (h1 : Tr Envs C x) (h2 : Tr Envs C y) : Tr Envs C (meet x y) := by
  intro Ψ hΨ γ w hw
  rw [meet_assoc, h1 Ψ hΨ _ w hw, h2 Ψ hΨ γ w hw]

theorem lemma3 {Envs : Env W D → Prop} {C : W → Prop}
    (hfin : ∃ L : List (Val W D), ∀ x, Tr Envs C x → x ∈ L) :
    ∃ x, IsLC Envs C x := by
  obtain ⟨L, hL⟩ := hfin
  obtain ⟨b, hb, hbL⟩ := fold_bottom (α := Val W D) meet top (Tr Envs C) le
    (tr_top Envs C) (fun _ _ h1 h2 => lemma2 h1 h2) le_meet_left le_meet_right
    (fun _ _ _ => le_trans) L
  exact ⟨b, hb, fun y hy => hbL y (hL y hy) hy⟩

theorem lemma4 {Envs : Env W D → Prop} (hE : ∀ Ψ, Envs Ψ → Ext Ψ) {C : W → Prop}
    (hloc : ∀ w, C w → ∃ s : D → Bool,
      Tr Envs (fun v => v = w) (fun _ => s) ∧
      ∀ y, Tr Envs (fun v => v = w) y → ∀ d, s d = true → y w d = true) :
    ∃ x, IsLC Envs C x := by
  classical
  have hex : ∀ w, ∃ s : D → Bool, C w → (Tr Envs (fun v => v = w) (fun _ => s) ∧
      ∀ y, Tr Envs (fun v => v = w) y → ∀ d, s d = true → y w d = true) := by
    intro w
    by_cases h : C w
    · obtain ⟨s, hs⟩ := hloc w h
      exact ⟨s, fun _ => hs⟩
    · exact ⟨fun _ => false, fun h' => absurd h' h⟩
  let f : W → D → Bool := fun w => Classical.choose (hex w)
  have hf : ∀ w, C w → (Tr Envs (fun v => v = w) (fun _ => f w) ∧
      ∀ y, Tr Envs (fun v => v = w) y → ∀ d, f w d = true → y w d = true) :=
    fun w => Classical.choose_spec (hex w)
  let x : Val W D := fun w d => if C w then f w d else false
  refine ⟨x, ?_, ?_⟩
  · intro Ψ hΨ γ w hw
    have h1 := (hf w hw).1 Ψ hΨ γ w rfl
    rw [← h1]
    apply hE Ψ hΨ
    funext d
  ...

/-- Lemma 1 / Existence theorem 16(a): local contexts exist in the propositional fragment. -/
theorem lc_exists_prop_i (I : Nat → W → Bool) (K : List Frame) (C : W → Prop) :
    ∃ x, LC.IsLC (EnvI I K) C x := ⟨_, LC.lemma1 (envI_ext I K) C⟩

theorem lc_exists_prop_s (I : Nat → W → Bool) (K : List Frame) (C : W → Prop) :
    ∃ x, LC.IsLC (EnvS I K) C x := ⟨_, LC.lemma1 (envS_ext I K) C⟩

theorem existence {Envs : Env W D → Prop} (hE : ∀ Ψ, Envs Ψ → Ext Ψ)
    (hD : ∃ L : List (D → Bool), ∀ s, s ∈ L) (C : W → Prop) :
    ∃ x, IsLC Envs C x := by
  obtain ⟨L, hL⟩ := hD
  apply lemma4 hE
  intro w _
  obtain ⟨s, hs, hmin⟩ := fold_bottom (α := D → Bool) (fun a b d => a d && b d) (fun _ => true)
    (fun s => Tr Envs (fun v => v = w) (fun _ => s)) (fun a b => ∀ d, a d = true → b d = true)
    (tr_top Envs (fun v => v = w))
    (by
      intro a b ha hb
      exact lemma2 ha hb)
    (by intro a b d h; simp at h; exact h.1)
    (by intro a b d h; simp at h; exact h.2)
    (by intro a b c h1 h2 d h; exact h2 d (h1 d h)) L
  refine ⟨s, hs, ?_⟩
  intro y hy d hd
  have hyc : Tr Envs (fun v => v = w) (fun _ => y w) := by
    intro Ψ hΨ γ v hv
    subst hv
    rw [← hy Ψ hΨ γ v rfl]
    apply hE Ψ hΨ
    funext d'; simp [meet]
  exact hmin (y w) (hL _) hyc d hd

/-- Lemma 5: when the local context `x` exists, `Sat ⇔ Sat'`. -/
theorem lemma5 {Envs : Env W D → Prop} (hE : ∀ Ψ, Envs Ψ → Ext Ψ) {C : W → Prop}
    {x : Val W D} (hx : IsLC Envs C x) (d : Val W D) : SatLC x d ↔ SatP Envs C d := by
  constructor
  · intro h
    refine ⟨x, hx.1, ?_⟩
    intro X' hle _ w _ e hX'
    exact h w e (hle w e hX')
  · intro h
    exact hx.2 d ((thm21 hE d).mp h)

/-- Lemma 5 (propositional fragment): `Sat ⇔ Sat'` -/
theorem lemma5_prop_i (I : Nat → W → Bool) (C : W → Prop) (F : Form) (hE : Expressive I) :
    SatI I C F ↔ SatI' I C F := by
  constructor
  · rintro H t ht
    obtain ⟨x, hx, hle⟩ := H t ht
    exact (LC.lemma5 (envI_ext I t.1) hx _).mp hle
  · intro H t ht
    obtain ⟨x, hx⟩ := lc_exists_prop_i I t.1 C
    exact ⟨x, hx, (LC.lemma5 (envI_ext I t.1) hx _).mpr (H t ht)⟩

/-- 20a : `tr_i ⊆ tr_s` (the symmetric environments are among the incremental ones). -/
theorem thm20a {Es Ei : Env W D → Prop} (h : ∀ Ψ, Es Ψ → Ei Ψ) {C : W → Prop} {x : Val W D}
    (hx : Tr Ei C x) : Tr Es C x :=
  fun Ψ hΨ => hx Ψ (h Ψ hΨ)

/-- 20b/20c : if both local contexts exist, `lc_s ≤ lc_i`, and `Sat_i → Sat_s`. -/
theorem thm20bc {Es Ei : Env W D → Prop} (h : ∀ Ψ, Es Ψ → Ei Ψ) {C : W → Prop}
    {xs xi : Val W D} (hs : IsLC Es C xs) (hi : IsLC Ei C xi) (d : Val W D) :
    le xs xi ∧ (SatLC xi d → SatLC xs d) :=
  ⟨hs.2 xi (thm20a h hi.1), fun H => le_trans (hs.2 xi (thm20a h hi.1)) H⟩

theorem thm20_prop (I : Nat → W → Bool) (hE : Expressive I) (C : W → Prop) (F : Form) :
    SatI I C F → SatS I C F := by
  intro H t ht
  obtain ⟨xi, hi, hle⟩ := H t ht
  obtain ⟨xs, hs⟩ := lc_exists_prop_s I t.1 C
  exact ⟨xs, hs, (LC.thm20bc (envS_sub_envI I t.1) hs hi _).2 hle⟩

theorem transpI_transpS (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    TranspI I C F → TranspS I C F :=
  fun h t ht γ w hw => h t ht t.1 (forall₂_same_refl _) γ w hw

/-- Theorem 21(i): `Sat' ⇔ Transp`, where `Transp` is `Tr Envs C d`. -/
theorem thm21 {Envs : Env W D → Prop} (hE : ∀ Ψ, Envs Ψ → Ext Ψ) {C : W → Prop}
    (d : Val W D) : SatP Envs C d ↔ Tr Envs C d := by
  constructor
  · rintro ⟨X, hX, hX'⟩
    have hle : cle C X d := hX' X (le_refl X) hX
    intro Ψ hΨ γ w hw
    have h1 := hX Ψ hΨ (meet d γ) w hw
    have h2 := hX Ψ hΨ γ w hw
    rw [← h2, ← h1]
    apply hE Ψ hΨ
    funext e
    have := hle w hw e
    by_cases hx : X w e = true
    · have := this hx; simp [meet, hx, this]
    · have : X w e = false := by simpa using hx
      simp [meet, this]
  · intro h
    refine ⟨d, h, ?_⟩
    intro X' hle _ w _ e hx
    exact hle w e hx

/-- Theorem 21(ii), incremental, propositional fragment. -/
theorem thm21_prop_i (I : Nat → W → Bool) (hE : Expressive I) (C : W → Prop) (F : Form) :
    SatI' I C F ↔ TranspI I C F := by
  constructor
  · intro H t ht K' hK γ w hw
    exact (bridge_i I hE C t.1 t.2.1).mp ((LC.thm21 (envI_ext I t.1) (dval I t.2.1)).mp (H t ht)) K' hK γ w hw
  · intro H t ht
    exact (LC.thm21 (envI_ext I t.1) (dval I t.2.1)).mpr ((bridge_i I hE C t.1 t.2.1).mpr (H t ht))

theorem thm21_prop_s (I : Nat → W → Bool) (hE : Expressive I) (C : W → Prop) (F : Form) :
    SatS' I C F ↔ TranspS I C F := by
  constructor
  · intro H t ht γ w hw
    exact (bridge_s I hE C t.1 t.2.1).mp ((LC.thm21 (envS_ext I t.1) (dval I t.2.1)).mp (H t ht)) γ w hw
  · intro H t ht
    exact (LC.thm21 (envS_ext I t.1) (dval I t.2.1)).mpr ((bridge_s I hE C t.1 t.2.1).mpr (H t ht))

theorem thm22_prop (I : Nat → W → Bool) (hE : Expressive I) (C : W → Prop) (F : Form) :
    (SatI I C F ↔ SatI' I C F) ∧ (SatI' I C F ↔ dyn I F C ≠ none) :=
  ⟨lemma5_prop_i I C F hE, (thm21_prop_i I hE C F).trans (theorem1 I C F).1⟩

theorem example23a : ¬ ∃ x, LC.IsLC Envs C x := by
  rintro ⟨x, hx, hmin⟩
  have hx' := (tr_iff x).mp hx
  -- x is infinite
  have hinf : Inf (x ()) := by
    have := (hx' (fun _ => true)).mpr (by intro N; exact ⟨N, Nat.le_refl _, rfl⟩)
    simpa using this
  obtain ⟨a, _, ha⟩ := hinf 0
  -- remove one element
  let y : LC.Val Unit Nat := fun _ d => x () d && decide (d ≠ a)
  have hy : LC.Tr Envs C y := by
    rw [tr_iff]
    intro γ
    have h1 := hx' γ
    refine Iff.trans ?_ h1
    apply inf_congr_iff _ _ a
    intro m hm
    simp [y, hm]
  have := hmin y hy () a ha
  simp [y] at this

theorem example23b :
    LC.Tr Envs C Qinf ∧ LC.SatP Envs C Qinf ∧ ¬ (∀ d : Nat, Qinf () d = true) := by
  have hT : LC.Tr Envs C Qinf := by
    rw [tr_iff]
    intro γ
    apply inf_congr_iff _ _ 0
    intro m hm
    simp [Qinf, hm]
  refine ⟨hT, (LC.thm21 (by rintro Ψ rfl; exact Ψinf_ext) Qinf).mpr hT, ?_⟩
  intro h; have := h 0; simp [Qinf] at this

/-- items 30: if each symbol occurs at most once, Super = Kleene (= standard Kleene). -/
theorem lemma6 (I : Nat → W → Bool) (F : Form) (hL : LinK symS F) (w : W) :
    Super I F w = Kleene I F w := by
  unfold Super
  rw [valOpt_vk_sk I symS F hL w, theorem41]

/-- **Lemma 7**: if `Kleene(F,w) ≠ #` then `Super(F,w) = Kleene(F,w)`. -/
theorem lemma7 (I : Nat → W → Bool) (F : Form) (w : W) (h : Kleene I F w ≠ none) :
    Super I F w = Kleene I F w := by
  cases hk : Kleene I F w with
  | none => exact absurd hk h
  | some v =>
    have h1 := (valOpt_eq_some _ _).mp hk
    unfold Super
    rw [valOpt_eq_some]
    obtain ⟨v0, hv0⟩ := VK_nonempty I symS F w
    have h0 := vk_sym_sub_tok I F w v0 hv0
    have hv : v0 = v := by
      cases v <;> cases v0 <;> simp_all
    subst hv
    exact ⟨hv0, fun h' => h1.2 (vk_sym_sub_tok I F w _ h')⟩

/-- Lemma 8(i) (incremental) -/
theorem lemma8_i_super (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    KleeneAccI I C F → SuperAccI I C F := by
  intro h t ht K' hK w hw
  have := h t ht K' hK w hw
  rw [lemma7 I _ w this]; exact this

/-- Lemma 8(i) (symmetric) -/
theorem lemma8_s_super (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    KleeneAccS I C F → SuperAccS I C F := by
  intro h w hw
  have := h w hw
  rw [lemma7 I _ w this]; exact this

/-- Lemma 8(ii), incremental -/
theorem lemma8_i_eq (I : Nat → W → Bool) (C : W → Prop) (F : Form) (h : KleeneAccI I C F) :
    ∀ w, C w → Kleene I F w = Super I F w :=
  lemma8_s_eq I C F (kleeneAccI_S I C F h)

/-- Lemma 8(ii), symmetric -/
theorem lemma8_s_eq (I : Nat → W → Bool) (C : W → Prop) (F : Form) (h : KleeneAccS I C F) :
    ∀ w, C w → Kleene I F w = Super I F w :=
  fun w hw => (lemma7 I F w (h w hw)).symm

/-- `Kleene-accept_i ⇒ Kleene-accept_s` (used in the proof of Lemma 8(ii) for `v = i`). -/
theorem kleeneAccI_S (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    KleeneAccI I C F → KleeneAccS I C F := by
  intro h w hw
  have hl := superAcc_lcCond I F C (lemma8_i_super I C F h)
  rw [theorem41, lemmaY I F C hl w hw]; simp

theorem theorem36 (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    (KleeneAccI I C F ↔ SuperAccI I C F) ∧
    (KleeneAccI I C F → ∀ w, C w → Kleene I F w = Super I F w) :=
  ⟨⟨lemma8_i_super I C F, fun h => lcCond_kleeneAccI I C F (superAcc_lcCond I F C h)⟩,
   lemma8_i_eq I C F⟩

theorem prop_fragment_collapse (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    (TranspI I C F ↔ dyn I F C ≠ none) ∧ (KleeneAccI I C F ↔ TranspI I C F) ∧
    (SuperAccI I C F ↔ TranspI I C F) := by
  refine ⟨(theorem1 I C F).1, ⟨fun h => ?_, fun h => (theorem38a I C F h).1⟩,
    ⟨fun h => ?_, fun h => (theorem38a I C F h).2⟩⟩
  · exact (transpI_iff_lcCond I C F).mpr (superAcc_lcCond I F C (lemma8_i_super I C F h))
  · exact (transpI_iff_lcCond I C F).mpr (superAcc_lcCond I F C h)

/-- Lemma 8(i) (symmetric) -/
theorem lemma8_s_super (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    KleeneAccS I C F → SuperAccS I C F := by
  intro h w hw
  have := h w hw
  rw [lemma7 I _ w this]; exact this

/-- Lemma 11, positive half: `(pp' or not pp')` is symmetrically super-acceptable everywhere. -/
theorem lemma11_super (I : Nat → W → Bool) (a b : Nat) (C : W → Prop) :
    SuperAccS I C (exF a b) := by
  intro w _
  have : Super I (exF a b) w = some true := by
    rw [super_eq_some_iff]
    intro ρ _
    simp only [exF, evK, Bop.eval]
    cases ρ (symS.κ a b 0) w <;> rfl
  rw [this]; simp

/-- Lemma 11, negative half: if `p` is false somewhere in `C` it is not Kleene-acceptable. -/
theorem lemma11_not_kleene (I : Nat → W → Bool) (a b : Nat) (C : W → Prop) (w : W)
    (hw : C w) (hp : I a w = false) : ¬ KleeneAccS I C (exF a b) := by
  intro h
  have := h w hw
  rw [theorem41] at this
  simp [exF, sk, hp, skop] at this

/-- **Theorem 38a** (propositional fragment): `Transp_i ⇒ Kleene-accept_i` (and Super-accept_i). -/
theorem theorem38a (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    TranspI I C F → KleeneAccI I C F ∧ SuperAccI I C F := by
  intro h
  have h1 := lcCond_kleeneAccI I C F ((transpI_iff_lcCond I C F).mp h)
  exact ⟨h1, lemma8_i_super I C F h1⟩

theorem theorem38b_39b :
    Det (VP P2 Q2 Q2') ∧ ¬ transNo P2 Q2 ∧ ¬ dynDefined P2 Q2 :=
  ⟨ex_kleene_acceptable, ex_not_transparent, ex_dynamic_undefined⟩

/-- more precisely the sentence is Kleene-false (and super-false) in the context (not `#`) -/
theorem ex_value_false : valOpt (VP P2 Q2 Q2') = some false := by
  rw [valOpt_eq_some]
  have h := (kleeneNo_iff P2 Q2 Q2').mpr (Or.inl ⟨1, rfl, by simp [Q2], by simp [Q2']⟩)
  refine ⟨⟨fun d => Q2 d && Q2' d, fun d hq => by simp [hq], ?_⟩, ?_⟩
  · have : ¬ quant fNo P2 (fun d => Q2 d && Q2' d) = true := by
      rw [quantNo_iff]; intro hh; apply hh 1; simp [P2, Q2, Q2']
    simpa using this
  · rintro ⟨ρ, hρ, hv⟩
    have : quant fNo P2 ρ = true := hv
    rw [quantNo_iff] at this
    exact this 1 ⟨rfl, by rw [hρ 1 (by simp [Q2])]; simp [Q2']⟩

theorem kleeneNo_iff {n : Nat} (P Q Q' : Pred n) :
    Det (VP P Q Q') ↔ (∃ d, P d = true ∧ Q d = true ∧ Q' d = true) ∨ dynDefined P Q := by
  unfold Det
  constructor
  · intro h
    refine Classical.byContradiction (fun hne => ?_)
    have h1 : ¬ ∃ d, P d = true ∧ Q d = true ∧ Q' d = true := fun h' => hne (Or.inl h')
    have h2 : ¬ dynDefined P Q := fun h' => hne (Or.inr h')
    obtain ⟨d1, hd1P, hd1Q⟩ : ∃ d, P d = true ∧ Q d = false := by
      refine Classical.byContradiction (fun hh => h2 (fun d hP => ?_))
      by_cases hq : Q d = true
      · exact hq
      · exact absurd ⟨d, hP, by simpa using hq⟩ hh
    have t : VP P Q Q' true := by
      refine ⟨fun d => Q d && Q' d, fun d hq => by simp [hq], ?_⟩
      rw [quantNo_iff]; intro d ⟨hp, hq⟩
      simp at hq; exact h1 ⟨d, hp, hq.1, hq.2⟩
    have f : VP P Q Q' false := by
      refine ⟨fun d => if Q d then Q' d else true, fun d hq => by simp [hq], ?_⟩
      have : ¬ quant fNo P (fun d => if Q d then Q' d else true) = true := by
        rw [quantNo_iff]; intro hh; apply hh d1; simp [hd1P, hd1Q]
      simpa using this
    rcases h with ⟨_, h⟩ | ⟨_, h⟩
    · exact h f
  ...

theorem theorem39a :
    TranspS I39 (fun _ => True) F39 ∧ ¬ KleeneAccS I39 (fun _ => True) F39 ∧
    ¬ SuperAccS I39 (fun _ => True) F39 := by
  refine ⟨?_, ?_, ?_⟩
  · intro t ht γ w _
    simp only [F39, occs, List.mem_append, List.mem_map, List.mem_singleton] at ht
    rcases ht with ⟨u, hu, rfl⟩ | ⟨u, hu, rfl⟩
    · have hu' : u = ([], 0, 1, 0) := by simpa [occs] using hu
      subst hu'
      cases w <;> simp [plug, Frame.fill, ev, I39, Bop.eval]
    · have hu' : u = ([], 2, 3, 0) := by simpa [occs] using hu
      subst hu'
      cases w <;> simp [plug, Frame.fill, ev, I39, Bop.eval]
  · intro h
    have := h false trivial
    rw [theorem41] at this
    simp [F39, sk, I39, skop] at this
  · intro h
    have := h false trivial
    have hL : LinK symS F39 := by
      simp [F39, LinK, keys, symS]
    unfold SuperAccS at h
    rw [show Super I39 F39 false = Kleene I39 F39 false from lemma6 I39 F39 hL false,
      theorem41] at this
  ...

theorem theorem38b_39b :
    Det (VP P2 Q2 Q2') ∧ ¬ transNo P2 Q2 ∧ ¬ dynDefined P2 Q2 :=
  ⟨ex_kleene_acceptable, ex_not_transparent, ex_dynamic_undefined⟩

theorem theorem41 (I : Nat → W → Bool) (F : Form) (w : W) : Kleene I F w = sk I F w := by
  unfold Kleene
  rw [valOpt_vk_sk I tokS _ (linK_numF F 0) w, sk_numF]