KRF.gamma_to_theta_injRed

import Definitions.Def_KRF_Machinery
noncomputable section
open KRFCore
open KRFCore.FStruct
open KRF
variable {σD σQ : Sig}
def InjectiveReduction {Q : QueryLanguage σQ} (Γ Γ₀ : Krf σD σQ Q) : Prop :=
  ∃ r : Reduction Γ Γ₀, Function.Injective (r.p)
/-- 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.gamma_to_theta_injRed {Q : QueryLanguage σQ} (c : Coding σD σQ) (S : StarContract σD σQ Q)
    (Γ : Krf σD σQ Q) (hΓ : Universal Γ) :
    ∃ T : Krf σD σQ Q, IsTheta c S T ∧ InjectiveReduction T Γ :=
  sorry