defn trm : prop
   | lam = (trm -> trm) -> trm
   | app = trm -> trm -> trm

defn linear : (trm -> trm) -> prop
   | linear_var = linear (λ V : trm . V )