Compiler HO-unif-for free

[FissoreD]

• Instance compilation
  • maybe-beta, e.g. in fun x => f x (A x) we detect A x
  • maybe-eta, e.g. fun x => f (A x) is a maybe-eta (+ A x is a maybe-beta)
  • maybe-llam, e.g. F a b is a maybe-llam
• Goal compilation
  • maybe-beta, e.g. in fun x => f x (A x) we detect A x
  • maybe-eta, e.g. fun x => f (A x) is a maybe-eta (+ A x is a maybe-beta)
  • maybe-llam, e.g. F a b is a maybe-llam

The main difference between instance and goal compilation is that in the instance we work on a closed term.
In the goal, we can have coq unification variables.