import PropSyntax
import LCAbstract
/-!
# Propositional fragment: dynamic semantics, Transparency, local contexts
Appendix items 6, 7-9 (Theorem 1), 10-12, 16(a), 17-22 restricted to the propositional fragment.
-/
namespace LCProp
variable {W : Type}

/-! ## Item 6: dynamic semantics (propositional part) -/
/-- context in which the second argument of `o` is interpreted -/
def Bop.ctx (o : Bop) (C D : W → Prop) : W → Prop :=
  match o with
  | .and => D
  | .or => fun w => C w ∧ ¬ D w
  | .imp => D

/-- how the output context is assembled (`D = C[F]`, `E = ctx[G]`) -/
def Bop.comb (o : Bop) (C D E : W → Prop) : W → Prop :=
  match o with
  | .and => E
  | .or => fun w => D w ∨ E w
  | .imp => fun w => C w ∧ ¬ (D w ∧ ¬ E w)

open Classical in
/-- `dyn I F C = none` is `C[F] = #`. -/
noncomputable def dyn (I : Nat → W → Bool) : Form → (W → Prop) → Option (W → Prop)
  | .atom a, C => some (fun w => C w ∧ I a w = true)
  | .trig a b _, C =>
      if ∀ w, C w → I a w = true then some (fun w => C w ∧ I b w = true) else none
  | .neg F, C => (dyn I F C).map (fun D w => C w ∧ ¬ D w)
  | .bin o F G, C => (dyn I F C).bind (fun D => (dyn I G (o.ctx C D)).map (o.comb C D))

/-! ## local contexts of an occurrence, computed syntactically -/
def Frame.step (I : Nat → W → Bool) (C : W → Prop) : Frame → (W → Prop)
  | .neg => C
  | .left _ _ => C
  | .right o F => fun w => C w ∧ ev I F w = o.need

def lcK (I : Nat → W → Bool) : (W → Prop) → List Frame → (W → Prop)
  | C, [] => C
  | C, f :: K => lcK I (f.step I C) K

theorem lcK_sub (I : Nat → W → Bool) : ∀ (K : List Frame) (C : W → Prop) (w : W),
    lcK I C K w → C w := by
  intro K
  induction K with
  | nil => intro C w h; exact h
  | cons f K ih =>
    intro C w h
    have := ih _ _ h
    cases f <;> simp [Frame.step] at this <;> first | exact this | exact this.1

theorem lcK_congr (I : Nat → W → Bool) : ∀ (K : List Frame) (C C' : W → Prop),
    (∀ w, C w ↔ C' w) → ∀ w, lcK I C K w ↔ lcK I C' K w := by
  intro K
  induction K with
  | nil => intro C C' h w; exact h w
  | cons f K ih =>
    intro C C' h w
    apply ih
    intro v
    cases f <;> simp [Frame.step, h v]

/-! ## Transparency (items 7-8) -/
/-- `Transp_i(C,F)`: every trigger occurrence, every good final, every `γ`. -/
def TranspI (I : Nat → W → Bool) (C : W → Prop) (F : Form) : Prop :=
  ∀ t ∈ occs F, ∀ K', F2 Frame.same t.1 K' → ∀ γ : Form, ∀ w, C w →
    ev I (plug K' (.bin .and (.atom t.2.1) γ)) w = ev I (plug K' γ) w

/-- `Transp_s(C,F)`: the good final is the actual one. -/
def TranspS (I : Nat → W → Bool) (C : W → Prop) (F : Form) : Prop :=
  ∀ t ∈ occs F, ∀ γ : Form, ∀ w, C w →
    ev I (plug t.1 (.bin .and (.atom t.2.1) γ)) w = ev I (plug t.1 γ) w

theorem forall₂_same_refl : ∀ K : List Frame, F2 Frame.same K K := by
  intro K
  induction K with
  | nil => exact F2.nil
  | cons f K ih =>
    refine F2.cons ?_ ih
    cases f <;> simp [Frame.same]

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

/-! ### Lemma: transparency of one occurrence = presupposition entailed by the local context -/
theorem Bop.const_of_ne_need (o : Bop) (e b1 b2 : Bool) (h : e ≠ o.need) :
    o.eval e b1 = o.eval e b2 := by
  cases o <;> cases e <;> simp [Bop.eval, Bop.need] at * 

theorem applyK_fwd (I : Nat → W → Bool) (a : Nat) :
    ∀ (K K' : List Frame), F2 Frame.same K K' → ∀ (C : W → Prop) (w : W), C w →
      (lcK I C K w → I a w = true) → ∀ g : Bool, applyK I w K' (I a w && g) = applyK I w K' g := by
  intro K K' h
  induction h with
  | nil =>
    intro C w hC hyp g
    have := hyp hC
    simp [applyK, this]
  | @cons f f' K K' hs _ ih =>
    intro C w hC hyp g
    rcases Frame.same_cases hs with ⟨rfl, rfl⟩ | ⟨o, G, G', rfl, rfl⟩ | ⟨o, F, rfl, rfl⟩
    · simp only [applyK, Frame.fn]
      rw [ih C w hC hyp g]
    · simp only [applyK, Frame.fn]
      rw [ih C w hC hyp g]
    · by_cases hF : ev I F w = o.need
      · simp only [applyK, Frame.fn]
        rw [ih (Frame.step I C (.right o F)) w ⟨hC, hF⟩ hyp g]
      · simp only [applyK, Frame.fn]
        exact Bop.const_of_ne_need o _ _ _ hF

def nform (o : Bop) : Form := if o.neut then Form.tt else Form.ff

theorem ev_nform (I : Nat → W → Bool) (w : W) (o : Bop) : ev I (nform o) w = o.neut := by
  cases o <;> simp [nform, Bop.neut, ev_tt, ev_ff]

theorem nform_trigFree (o : Bop) : (nform o).trigFree := by
  cases o <;> simp [nform, Bop.neut, Form.tt_trigFree, Form.ff_trigFree]

/-- for a world in the local context there is a good final making the hole "visible" -/
theorem exists_inj (I : Nat → W → Bool) : ∀ (K : List Frame) (C : W → Prop) (w : W), lcK I C K w →
    ∃ K', F2 Frame.sameTF K K' ∧ ∀ b1 b2, applyK I w K' b1 = applyK I w K' b2 → b1 = b2 := by
  intro K
  induction K with
  | nil => intro C w _; exact ⟨[], F2.nil, fun b1 b2 h => h⟩
  | cons f K ih =>
    intro C w h
    obtain ⟨K'', hK'', hinj⟩ := ih (f.step I C) w h
    have hstep : f.step I C w := lcK_sub I K _ w h
    cases f with
    | neg =>
      refine ⟨Frame.neg :: K'', F2.cons ⟨trivial, trivial⟩ hK'', ?_⟩
      intro b1 b2 hb
      simp only [applyK, Frame.fn] at hb
      apply hinj
      cases hx : applyK I w K'' b1 <;> cases hy : applyK I w K'' b2 <;> simp_all
    | left o G =>
      refine ⟨Frame.left o (nform o) :: K'', F2.cons ⟨rfl, nform_trigFree o⟩ hK'', ?_⟩
      intro b1 b2 hb
      simp only [applyK, Frame.fn, ev_nform] at hb
      apply hinj
      cases o <;> cases hx : applyK I w K'' b1 <;> cases hy : applyK I w K'' b2 <;>
        simp_all [Bop.eval, Bop.neut]
    | right o F =>
      refine ⟨Frame.right o F :: K'', F2.cons ⟨⟨rfl, rfl⟩, trivial⟩ hK'', ?_⟩
      intro b1 b2 hb
      have hF : ev I F w = o.need := hstep.2
      simp only [applyK, Frame.fn, hF] at hb
      apply hinj
      cases o <;> cases hx : applyK I w K'' b1 <;> cases hy : applyK I w K'' b2 <;>
        simp_all [Bop.eval, Bop.need]

theorem forall₂_sameTF_same : ∀ {K K' : List Frame}, F2 Frame.sameTF K K' →
    F2 Frame.same K K' := by
  intro K K' h
  induction h with
  | nil => exact F2.nil
  | cons hf _ ih => exact F2.cons hf.1 ih

/-- One occurrence: transparent iff its presupposition holds throughout the local context. -/
theorem local_iff (I : Nat → W → Bool) (C : W → Prop) (K : List Frame) (a : Nat) :
    (∀ K', F2 Frame.same K K' → ∀ γ : Form, ∀ w, C w →
      ev I (plug K' (.bin .and (.atom a) γ)) w = ev I (plug K' γ) w) ↔
    ∀ w, lcK I C K w → I a w = true := by
  constructor
  · intro H w hw
    obtain ⟨K', hK', hinj⟩ := exists_inj I K C w hw
    have hC := lcK_sub I K C w hw
    have := H K' (forall₂_sameTF_same hK') Form.tt w hC
    rw [ev_plug, ev_plug] at this
    simp only [ev, Bop.eval, ev_tt, Bool.and_true] at this
    refine Classical.byContradiction (fun hne => ?_)
    have hf : I a w = false := by simpa using hne
    rw [hf] at this
    have := hinj _ _ this
    simp at this
  · intro H K' hK' γ w hw
    rw [ev_plug, ev_plug]
    simp only [ev, Bop.eval]
    exact applyK_fwd I a K K' hK' C w hw (H w) _

/-! ## Theorem 1 -/
theorem comb_iff (o : Bop) (C D E : W → Prop) (w : W) (bF bG : Bool)
    (h2 : D w ↔ (C w ∧ bF = true)) (h1 : E w ↔ (o.ctx C D w ∧ bG = true)) :
    o.comb C D E w ↔ (C w ∧ o.eval bF bG = true) := by
  cases o <;> by_cases hC : C w <;> cases bF <;> cases bG <;>
    simp_all [Bop.comb, Bop.ctx, Bop.eval]

theorem dyn_iff (I : Nat → W → Bool) : ∀ (F : Form) (C : W → Prop),
    ((dyn I F C).isSome = true ↔ ∀ t ∈ occs F, ∀ w, lcK I C t.1 w → I t.2.1 w = true) ∧
    ∀ D, dyn I F C = some D → ∀ w, D w ↔ (C w ∧ ev I F w = true) := by
  intro F
  induction F with
  | atom a =>
    intro C
    refine ⟨?_, ?_⟩
    · simp [dyn, occs]
    · intro D hD w
      simp [dyn] at hD
      subst hD; simp [ev]
  | trig a b k =>
    intro C
    by_cases h : ∀ w, C w → I a w = true
    · have hd : dyn I (.trig a b k) C = some (fun w => C w ∧ I b w = true) := by
        simp only [dyn]; exact if_pos h
      refine ⟨?_, ?_⟩
      · rw [hd]
        constructor
        · intro _ t ht w hw
          simp [occs] at ht; subst ht; exact h w hw
        · intro _; rfl
      · intro D hD w
        rw [hd] at hD
        have := Option.some.inj hD
        subst this
        constructor
        · rintro ⟨h1, h2⟩; exact ⟨h1, by simp [ev, h w h1, h2]⟩
        · rintro ⟨h1, h2⟩; refine ⟨h1, ?_⟩; simp [ev] at h2; exact h2.2
    · have hd : dyn I (.trig a b k) C = none := by
        simp only [dyn]; exact if_neg h
      refine ⟨?_, ?_⟩
      · rw [hd]
        constructor
        · intro h'; simp at h'
        · intro H; apply absurd _ h
          intro w hw; exact H ([], a, b, k) (by simp [occs]) w hw
      · intro D hD; rw [hd] at hD; simp at hD
  | neg F ih =>
    intro C
    obtain ⟨ih1, ih2⟩ := ih C
    refine ⟨?_, ?_⟩
    · simp only [dyn, occs]
      constructor
      · intro h
        have h' : (dyn I F C).isSome = true := by
          cases hh : dyn I F C <;> simp_all
        have := ih1.mp h'
        intro t ht w hw
        simp only [List.mem_map] at ht
        obtain ⟨u, hu, rfl⟩ := ht
        exact this u hu w hw
      · intro h
        have h' : ∀ t ∈ occs F, ∀ w, lcK I C t.1 w → I t.2.1 w = true := by
          intro t ht w hw
          exact h (Frame.neg :: t.1, t.2) (List.mem_map.mpr ⟨t, ht, rfl⟩) w hw
        have := ih1.mpr h'
        cases hh : dyn I F C <;> simp_all
    · intro D hD w
      simp only [dyn] at hD
      cases hh : dyn I F C with
      | none => simp [hh] at hD
      | some D0 =>
        simp [hh] at hD
        subst hD
        have := ih2 D0 hh w
        by_cases hC : C w <;> cases hf : ev I F w <;> simp_all [ev]
  | bin o F G ihF ihG =>
    intro C
    obtain ⟨ihF1, ihF2⟩ := ihF C
    have hoccs : ∀ P : List Frame × Nat × Nat × Nat → Prop,
        (∀ t ∈ occs (Form.bin o F G), P t) ↔
        ((∀ t ∈ occs F, P (Frame.left o G :: t.1, t.2)) ∧
         (∀ t ∈ occs G, P (Frame.right o F :: t.1, t.2))) := by
      intro P
      simp only [occs, List.mem_append, List.mem_map]
      constructor
      · intro h
        exact ⟨fun t ht => h _ (Or.inl ⟨t, ht, rfl⟩), fun t ht => h _ (Or.inr ⟨t, ht, rfl⟩)⟩
      · rintro ⟨h1, h2⟩ t (⟨u, hu, rfl⟩ | ⟨u, hu, rfl⟩)
        · exact h1 u hu
        · exact h2 u hu
    cases hF : dyn I F C with
    | none =>
      have hnF : ¬ (∀ t ∈ occs F, ∀ w, lcK I C t.1 w → I t.2.1 w = true) := by
        intro h; have := ihF1.mpr h; simp [hF] at this
      refine ⟨?_, ?_⟩
      · simp only [dyn, hF, Option.bind_none]
        constructor
        · intro h; simp at h
        · intro h; exact absurd ((hoccs _).mp h).1 hnF
      · intro D hD; simp [dyn, hF] at hD
    | some D =>
      have hD := ihF2 D hF
      have hFdef : ∀ t ∈ occs F, ∀ w, lcK I C t.1 w → I t.2.1 w = true := ihF1.mp (by simp [hF])
      have hctx : ∀ w, o.ctx C D w ↔ Frame.step I C (.right o F) w := by
        intro w
        have := hD w
        cases o <;> by_cases hC : C w <;> cases hf : ev I F w <;>
          simp_all [Bop.ctx, Frame.step, Bop.need]
      obtain ⟨ihG1, ihG2⟩ := ihG (o.ctx C D)
      have hGeq : ∀ t ∈ occs G, ∀ w, lcK I (o.ctx C D) t.1 w ↔
          lcK I C (Frame.right o F :: t.1) w := by
        intro t _ w
        exact lcK_congr I t.1 _ _ hctx w
      refine ⟨?_, ?_⟩
      · simp only [dyn, hF, Option.bind_some]
        rw [Option.isSome_map]
        rw [ihG1, hoccs]
        constructor
        · intro h
          refine ⟨fun t ht w hw => hFdef t ht w hw, fun t ht w hw => ?_⟩
          exact h t ht w ((hGeq t ht w).mpr hw)
        · rintro ⟨_, h2⟩ t ht w hw
          exact h2 t ht w ((hGeq t ht w).mp hw)
      · intro E hE w
        simp only [dyn, hF, Option.bind_some] at hE
        simp at hE
        obtain ⟨E0, hE0, rfl⟩ := hE
        have h1 := ihG2 E0 hE0 w
        exact comb_iff o C D E0 w _ _ (hD w) h1

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)

/-! ## Bridge to the abstract theory (items 10-22 for the propositional fragment) -/
/-- semantic effect of the string `α _ β'` (coded by the context `K'`) -/
def envOf (I : Nat → W → Bool) (K' : List Frame) : LC.Env W Unit :=
  fun x w => applyK I w K' (x w ())

def EnvI (I : Nat → W → Bool) (K : List Frame) : LC.Env W Unit → Prop :=
  fun Ψ => ∃ K', F2 Frame.same K K' ∧ Ψ = envOf I K'

def EnvS (I : Nat → W → Bool) (K : List Frame) : LC.Env W Unit → Prop :=
  fun Ψ => Ψ = envOf I K

/-- the presupposition `d` (proposition named `a`) as a restriction -/
def dval (I : Nat → W → Bool) (a : Nat) : LC.Val W Unit := fun w _ => I a w

theorem envOf_ext (I : Nat → W → Bool) (K : List Frame) : LC.Ext (envOf I K) := by
  intro x y w h
  simp [envOf, h]

theorem envI_ext (I : Nat → W → Bool) (K : List Frame) : ∀ Ψ, EnvI I K Ψ → LC.Ext Ψ := by
  rintro Ψ ⟨K', _, rfl⟩; exact envOf_ext I K'
theorem envS_ext (I : Nat → W → Bool) (K : List Frame) : ∀ Ψ, EnvS I K Ψ → LC.Ext Ψ := by
  rintro Ψ rfl; exact envOf_ext I K

theorem envS_sub_envI (I : Nat → W → Bool) (K : List Frame) : ∀ Ψ, EnvS I K Ψ → EnvI I K Ψ := by
  rintro Ψ rfl; exact ⟨K, forall₂_same_refl K, rfl⟩

theorem ev_and_plug (I : Nat → W → Bool) (K' : List Frame) (a : Nat) (γ : Form) (w : W) :
    ev I (plug K' (.bin .and (.atom a) γ)) w = applyK I w K' (I a w && ev I γ w) := by
  rw [ev_plug]; simp [ev, Bop.eval]

/-- `Transp_i(C, dd', α_β)` (item 57 of the main text) as `d ∈ tr_i(C, dd', α_β)`. -/
theorem bridge_i (I : Nat → W → Bool) (hE : Expressive I) (C : W → Prop) (K : List Frame) (a : Nat) :
    LC.Tr (EnvI I K) C (dval I a) ↔
    ∀ K', F2 Frame.same K K' → ∀ γ : Form, ∀ w, C w →
      ev I (plug K' (.bin .and (.atom a) γ)) w = ev I (plug K' γ) w := by
  constructor
  · intro H K' hK γ w hw
    have := H (envOf I K') ⟨K', hK, rfl⟩ (fun v _ => ev I γ v) w hw
    rw [ev_and_plug, ev_plug]
    simpa [envOf, LC.meet, dval] using this
  · rintro H Ψ ⟨K', hK, rfl⟩ γ' w hw
    obtain ⟨n, hn⟩ := hE (fun v => γ' v ())
    have := H K' hK (.atom n) w hw
    rw [ev_and_plug, ev_plug] at this
    have hn' : I n w = γ' w () := by rw [hn]
    simpa [envOf, LC.meet, dval, ev, hn'] using this

theorem bridge_s (I : Nat → W → Bool) (hE : Expressive I) (C : W → Prop) (K : List Frame) (a : Nat) :
    LC.Tr (EnvS I K) C (dval I a) ↔
    ∀ γ : Form, ∀ w, C w →
      ev I (plug K (.bin .and (.atom a) γ)) w = ev I (plug K γ) w := by
  constructor
  · intro H γ w hw
    have := H (envOf I K) rfl (fun v _ => ev I γ v) w hw
    rw [ev_and_plug, ev_plug]
    simpa [envOf, LC.meet, dval] using this
  · rintro H Ψ rfl γ' w hw
    obtain ⟨n, hn⟩ := hE (fun v => γ' v ())
    have := H (.atom n) w hw
    rw [ev_and_plug, ev_plug] at this
    have hn' : I n w = γ' w () := by rw [hn]
    simpa [envOf, LC.meet, dval, ev, hn'] using this

/-- Def. 17b (propositional fragment, local contexts exist): `Sat_i(C, F)` -/
def SatI (I : Nat → W → Bool) (C : W → Prop) (F : Form) : Prop :=
  ∀ t ∈ occs F, ∃ x, LC.IsLC (EnvI I t.1) C x ∧ LC.le x (dval I t.2.1)
/-- Def. 18b: `Sat'_i(C, F)` -/
def SatI' (I : Nat → W → Bool) (C : W → Prop) (F : Form) : Prop :=
  ∀ t ∈ occs F, LC.SatP (EnvI I t.1) C (dval I t.2.1)
def SatS (I : Nat → W → Bool) (C : W → Prop) (F : Form) : Prop :=
  ∀ t ∈ occs F, ∃ x, LC.IsLC (EnvS I t.1) C x ∧ LC.le x (dval I t.2.1)
def SatS' (I : Nat → W → Bool) (C : W → Prop) (F : Form) : Prop :=
  ∀ t ∈ occs F, LC.SatP (EnvS I t.1) C (dval I t.2.1)

/-- 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 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))

/-- 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)⟩

/-- Theorem 22 (propositional fragment, no side conditions needed):
`Sat_i ⇔ Sat'_i ⇔ Transp_i ⇔ C[F] ≠ #`. -/
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 20 (propositional fragment): incremental transparency implies symmetric transparency,
and incremental satisfaction implies symmetric satisfaction. -/
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⟩

end LCProp