fixity lambda lam
fixity lambda Π

defn tm : prop
   | p = tm
   | t = tm
   | lam = tm → (tm → tm) → tm
   | Π = tm → (tm → tm) → tm

fixity none 0 ::
defn :: : tm -> tm -> prop
   | p_t = p :: t
   | lam_pi =  [A : tm][T : tm -> tm][B : tm -> tm]
      ([x] x :: A -> T x :: B x )
      -> (lam x : A . T x) :: (Π x : A . B x)