fact: Definition class_provable (phi : minimalForm falsity_off) : Prop := nil ⊢C phi.
imports: Undecidability.DiophantineConstraints(H10C H10C_undec) Undecidability.FOL.Syntax(Core BinSig) Undecidability.Synthetic(Definitions Undecidability ReducibilityFacts)