let ExprF
= λ(a : Type) →
< LitF : { _1 : Natural }
| AddF : { _1 : a, _2 : a }
| MulF : { _1 : a, _2 : a }
>
in ExprF