data _implies_  (A B : Set ) : Set (succ Zero) where
  proof : ( A → B ) → A implies B