module sec9_2
imports prop-eval2 prop-desugar

rules
  DefT  : True() -> Impl(False(), False())

strategies
  eval1 = bottomup(try(Eval))
  eval2 = topdown(try(Eval))
  
  desugar2 = bottomup(try(DefI <+ DefE))

  impl-nf1 = topdown(repeat(DefT <+ DefN <+ DefA2 <+ DefO1 <+ DefE))
  impl-nf2 = topdown(try(DefT <+ DefN <+ DefA2 <+ DefO1 <+ DefE))