Expr: β-Reduction for ∏ binders?

Stream: lean4

[Max Nowak 🐺]

I have an expression e such as (m : Ty) -> Rest (i.e. a Expr.forallE), which I want to turn into Rest[m/mything], so basically just like β-Reduction for λ-Terms, just for ∏-Types this time. I'm doing some tactics programming. I forgot what this is even called :sweat_smile:

[Mario Carneiro]

If you have a forallE with no "loose bvars", then the binder is an open term with only the bvar index 0 in it. You can instantiate it using Expr.instantiate1

[Mario Carneiro]

Alternatively, you can "enter" the binder using forallMetaTelescope, which will automatically instantiate it with a fresh fvar. You can then substitute for that fvar using Expr.replaceFVar

[Max Nowak 🐺]

Thank you, that is exactly what I was looking for!