polyexpr
- Type: Constant, Variable, Type Function
- Expr: Constant, Variable, Function Application, Function Abstraction (Lambda)
Where we need this expression? Assertion, strategy?
Why dependent type?
Unit vs option?
Why we need parametric polymorphism? Strategy proof about generic type?