KRF.conj_self_entails

Proved

KRF.conj_self_entails

by jario · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Solution target of the arXiv 2412.11855 campaign (see the source reference for the mathematical statement).

Preamble

import Definitions.Def_KRF_Machinery
noncomputable section
open KRFCore
open KRFCore.FStruct
variable {σ : Sig}

Formal statement

theorem KRF.conj_self_entails {σ : Sig} (φ : Fm σ) :
    FStruct.Entails φ (Fm.conj φ φ) ∧ FStruct.Entails (Fm.conj φ φ) φ :=
  sorry

Source

arXiv 2412.11855v2 (Zhang, Jiang, Quan)