Flattening app/abs/arrow nodes in Reflection

[mtzguido]

This is not ready and CI will fail, but posting it here to keep track that we should probably do this eventually. The current errors I see are:

* Error 19 at typeclasses/Monad.fst(54,2-54,8):
  - Assertion failed
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - See also typeclasses/Monad.fst(54,9-54,72)

* Error 19 at typeclasses/Pulse.Class.BoundedIntegers.fst(59,25-59,26):
  - Assertion failed
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - See also typeclasses/Pulse.Class.BoundedIntegers.fst(12,53-12,69)

which I think stem from the change in encoding the lambdas in those classes.