data _implies_  (A B : Set ) : Set (succ Zero) where
  proof : ( A !$\rightarrow$! B ) !$\rightarrow$! A implies B