def LO.System.imply_boxdot_boxdot_of_imply_boxdot_plain {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢ ⊡φ ➝ ψ) : 𝓢 ⊢ ⊡φ ➝ ⊡ψ

Equations

• One or more equations did not get rendered due to their size.

theorem LO.System.imply_boxdot_boxdot_of_imply_boxdot_plain! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢! ⊡φ ➝ ψ) : 𝓢 ⊢! ⊡φ ➝ ⊡ψ

def LO.System.imply_boxdot_axiomT_of_imply_boxdot_boxdot {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢ ⊡φ ➝ ⊡ψ) : 𝓢 ⊢ ⊡φ ➝ □ψ ➝ ψ

Equations

• One or more equations did not get rendered due to their size.

theorem LO.System.imply_boxdot_axiomT_of_imply_boxdot_boxdot! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢! ⊡φ ➝ ⊡ψ) : 𝓢 ⊢! ⊡φ ➝ □ψ ➝ ψ

def LO.System.imply_box_box_of_imply_boxdot_axiomT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢ ⊡φ ➝ □ψ ➝ ψ) : 𝓢 ⊢ □φ ➝ □ψ

Equations

• LO.System.imply_box_box_of_imply_boxdot_axiomT h = LO.System.impTrans'' LO.System.imply_Box_BoxBoxdot (LO.System.impTrans'' (LO.System.implyBoxDistribute' h) LO.System.axiomL)

theorem LO.System.imply_box_box_of_imply_boxdot_axiomT! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢! ⊡φ ➝ □ψ ➝ ψ) : 𝓢 ⊢! □φ ➝ □ψ

theorem LO.System.imply_box_box_of_imply_boxdot_plain! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢! ⊡φ ➝ ψ) : 𝓢 ⊢! □φ ➝ □ψ

theorem LO.Modal.Hilbert.GL.imply_boxdot_plain_of_imply_box_box {φ ψ : Formula ℕ} : Hilbert.GL ℕ ⊢! □φ ➝ □ψ → Hilbert.GL ℕ ⊢! ⊡φ ➝ ψ

theorem LO.Modal.Hilbert.GL.unnecessitation! {φ : Formula ℕ} : Hilbert.GL ℕ ⊢! □φ → Hilbert.GL ℕ ⊢! φ

noncomputable instance LO.Modal.Hilbert.GL.instUnnecessitationNatFormula : System.Unnecessitation (Hilbert.GL ℕ)

Equations

• LO.Modal.Hilbert.GL.instUnnecessitationNatFormula = { unnec := fun {φ : LO.Modal.Formula ℕ} (h : LO.Modal.Hilbert.GL ℕ ⊢ □φ) => Nonempty.some ⋯ }