We start with a trivial language comtaining numbers and booleans.

> import Math
> import Data.List

> data UntypedTerm : Type where
>   CTrue : UntypedTerm
>   CFalse : UntypedTerm
>   IfThenElse : UntypedTerm -> UntypedTerm -> UntypedTerm -> UntypedTerm
>   CZero : UntypedTerm
>   Succ : UntypedTerm -> UntypedTerm
>   Pred : UntypedTerm -> UntypedTerm
>   IsZero : UntypedTerm -> UntypedTerm

We can create a generator for such terms:

> data UntypedTermGenerator : Nat -> List UntypedTerm -> Type where
>   GenEmpty : UntypedTermGenerator Z []
>   GenSucc : UntypedTermGenerator k xs -> UntypedTermGenerator (S k) ([CTrue,CFalse,CZero]) -- ++ (map ))

This generator in fact covers the UntypedTerms. First, we need a notion of the
size of a term

> size : UntypedTerm -> Nat
> size CTrue = 1
> size CFalse = 1
> size CZero = 1
> size (Succ t) = S (size t)
> size (Pred t) = S (size t)
> size (IsZero t) = S (size t)
> size (IfThenElse i t e) = S (plus (plus (size i) (size t)) (size e))

Since the terms form a tree there is a notion of depth:

> depth : UntypedTerm -> Nat
> depth CTrue = 1
> depth CFalse = 1
> depth CZero = 1
> depth (Succ t) = S (depth t)
> depth (Pred t) = S (depth t)
> depth (IsZero t) = S (depth t)
> depth (IfThenElse i t e) = S (maximum (maximum (depth i) (depth t)) (depth e))--S (maximum (maximum( (depth i) (depth t))) (depth e))

Now we can prove covering. We prove the equivalent result that for any Nat n and any UntypedTerm t with depth LTE n, then there exists an UntypedTermGenerator n xs such that Elem t xs.

> generatorCovers : (t:UntypedTerm) -> (xs : List UntypedTerm ** ((UntypedTermGenerator (depth t) xs), (Elem t xs)))--((n:Nat ** (UntypedTermGenerator n xs)) ** (Elem t xs))
> generatorCovers CTrue = ([CTrue,CFalse,CZero] ** (GenSucc GenEmpty,Here))
> generatorCovers CFalse = ([CTrue,CFalse,CZero] ** (GenSucc GenEmpty,There (the (Elem CFalse [CFalse,CZero]) Here)))
> generatorCovers (IfThenElse x y z) = ?generatorCovers_rhs_1
> generatorCovers CZero = ([CTrue,CFalse,CZero] ** (GenSucc GenEmpty,There (There (the (Elem CZero [CZero]) Here))))
> generatorCovers (Succ x) = ?generatorCovers_rhs_5
> generatorCovers (Pred x) = ?generatorCovers_rhs_6
> generatorCovers (IsZero x) = ?generatorCovers_rhs_7
