### Homework about inductive relations

Translate the typechecking of simply typed lambda calculus into Agda.

Automatic parameters become instance parameters:

    search1 : (P : a -> Type) -> {auto ans : P x} -> a

becomes

    search1 : {a : Set} (P : a → Set) {x} {{ans : P x}} → a

Note that Agda's instance resolution demands a unique answer, so
don't phrase any predicate with more than one proof.

Moreover, Agda does not recursively search the arguments of constructors
automatically. To search a constructor argument recursively, it must
be declared as an instance argument, inside double braces {{_}}.
For example,

    data PlaysAirGuitar : Name -> Type where
      GuitarButch1 : Happy Butch -> PlaysAirGuitar Butch

becomes

    data PlaysAirGuitar : Name -> Set where
      guitarButch1 : {{_ : Happy Butch}} -> PlaysAirGuitar Butch


Optional (term project idea):
Implement Fischer's CPS transformation as the inductive relation
CPS on types and the inductive relation cps on terms.

    ----------------------
    CPS r ℕ = (ℕ → r) → r

    CPS r a = (a' → r) → r     CPS r b = (b' → r) → r
    -------------------------------------------------
      CPS r (a → b) = ((a' → (b' → r) → r) → r) → r


    ---------------------
    cps (n : ℕ) = λk. k n

    ---------------
    cps x = λk. k x

                    cps t = t'
    ------------------------------------------
    cps (λx. t) = λk. k (λx. λdynk. t' dynk)


           cps s = s'              cps t = t'
    -----------------------------------------------------
    cps (s t) = λk. s' (λsval → t' (λtval → sval tval k))