a new strong-induction fold (less general)

- Make the well-foundedness proof of expr_acc transparent
- a record to wrap up the arguments in FoldApp