Propositional_Logic_Class.Classical_Logic_Completeness