KRF.thetaExpressiveComplete

import Definitions.Def_KRF_Machinery
noncomputable section
open KRFCore
open KRFCore.FStruct
open KRF
variable {σD σQ : Sig}
/-- The canonical-KRF predicate (platform form of thetaKrf): the theory
engine mapping carried by the StarContract. -/
def IsTheta {σD σQ : Sig} {Q : QueryLanguage σQ} (c : Coding σD σQ)
    (S : StarContract σD σQ Q) (T : Krf σD σQ Q) : Prop :=
  ∃ hdom : T.dom = S.isTheory,
    ∀ (π : Nat) (h : S.isTheory π), ∀ D φ,
      T.Γ π (hdom ▸ h) D φ ↔ KM (S.theoryEngine h) D φ

theorem KRF.thetaExpressiveComplete {Q : QueryLanguage σQ} (c : Coding σD σQ) (S : StarContract σD σQ Q) :
    ∃ T : Krf σD σQ Q, IsTheta c S T ∧ ExpressiveComplete T :=
  sorry