def Lean.Meta.Sym.DSimp.dsimpForall : DSimproc

Definitionally simplifies a forall expression.

Unlike Sym.Simp.simpForall, it descends into the binder type as well as the body.

Equations

• Lean.Meta.Sym.DSimp.dsimpForall e = Lean.Meta.Sym.DSimp.dsimpForall.go✝ e #[] false