SuccinctMCSP witness-class packaging -- proof internals

theorem Complexity.SuccinctMCSP.verifyRawWitness_eq_true_iff_internal (bits witness : List Bool) : verifyRawWitness bits witness = true ↔ RawWitnessRelation bits witness

theorem Complexity.SuccinctMCSP.rawWitnessRelation_mem_FNP_of_pairLang_mem_P_internal (hverifier : pairLang RawWitnessRelation ∈ P) : RawWitnessRelation ∈ FNP

theorem Complexity.SuccinctMCSP.mem_NP_of_pairLang_mem_P_internal (hwitness : NP.WitnessNTMConstruction) (hverifier : pairLang RawWitnessRelation ∈ P) : SuccinctMCSP ∈ NP