How exactly can λ-encoded datatypes be compiled to primitive operations?

Suppose you have the following compile target, optimized for performance:

```
data Term
= Var Int
| Lam Term
| App Term Term
| Nat Integer
| Add Term Term
| Mul Term Term

nf :: Term -> Term
```

I'm wondering how exactly, if possible, one could compile a Morte term to that language, reduce it, then read back to get a Morte term on the normal form. I think what is needed is something like that:

```
reduce :: Expr -> Expr -> Expr
reduce val typ = fromTerm typ . nf . toTerm $ val
```

So, `toTerm :: Expr -> Term` needs to erase the types, convert λ-encoded nats and nat operations to the respective primitives. `fromTerm :: Expr -> Term -> Expr` must re-add the types and convert native operations back to λ-encodings.
1. Is that correct?
2. Should primitive<->lambda conversions be based on syntactical equality? E.g., a term typed `∀ a . (a -> a) -> a -> a` becomes a `NAT`, the function `add : Nat -> Nat -> Nat` becomes `Add`?
3. Once it is done, how do I re-annotate the types?