Certificate theorem for N:

|- DeclAssum example_91_decls env ⇒ Eval env (Var "N") ((NUM --> NUM) N)

Definition of declaration list:

|- example_91_decls =
   [Dletrec
      [("N","v1",
        If (App (Opb Gt) (Var "v1") (Val (Lit (IntLit 100))))
          (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 10))))
          (App Opapp (Var "N")
             (App Opapp (Var "N")
                (App (Opn Plus) (Var "v1") (Val (Lit (IntLit 11)))))))]]