def Lean.Grind.nestedProof (p : Prop) (h : p) : p

A helper gadget for annotating nested proofs in goals.

Equations

• ⋯ = h

theorem Lean.Grind.nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq ⋯ ⋯