infixr -2 ->
defn -> : [a b: prop] prop
  as \a : prop . \b : prop . [ha : a] b

infixr -2 →
defn → : [a b: prop] prop 
  as (->)

infixl -3 <-
defn <- : [a b: prop] prop
  as \a : prop . \b : prop . b -> a

infixl -1 ←
defn → : [a b: prop] prop 
  as (<-)

infixr -2 =>
defn => : [a b: prop] prop
  as \a : prop . \b : prop . {ha : a} b

infixr -2 ⇒
defn ⇒ : [a b: prop] prop
  as (=>)

infixl -1 <=
defn <= : [b a : prop] prop
  as \a : prop . \b : prop . b => a

infixl -1 ⇐
defn ⇐ : [a b: prop] prop
  as (<=)


infixr 0 $
defn $ : {a b:prop} (a -> b) -> a -> b
  as ?\at bt : prop . \f . \ a : at . f a