AndrasKovacs

{-# OPTIONS --without-K #-}

{-
Below is an example of proving *everything* about the substitution calculus of a
simple TT with Bool.

The more challenging solution:
  - If substitutions are defined as lists of terms, then if you manage to
    prove that substitutions form a category, almost certainly you're done,
    since you can only prove this is you have all relevant lemmas.