caledon-2.0.0.0: examples/substitution.ncc

defn example : [ax : prop] ax -> prop
  as eximp = [atx : prop] example prop atx