From Undecidability Require Export FOL.Semantics FOL.Kripke FOL.Deduction.



About prv_min. About prv_into. About prv_class.
About valid. About kvalid.
About satis. About ksatis.