module G2Postulate

import G4LowerFormalPSpring
import G3MiddleFunctionsWinter

%access public export
%default total


-- 13
postulate not : GNat -> GNat
-- 15
postulate forall : GNat -> GNat -> GNat
-- 45
postulate proves : GNat -> GNat -> Bool

postulate r : GNat -> GNat




