test: nested proof propagation

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -366,6 +366,7 @@ where
           let c := args[0]!
           internalizeImpl c generation e
           registerParent e c
+          pushEqTrue c <| mkApp2 (mkConst ``eq_true) c args[1]!
         else if f.isConstOf ``ite && args.size == 5 then
           let c := args[1]!
           internalizeImpl c generation e

tests/lean/run/grind_nested_proofs.lean

@@ -36,3 +36,17 @@ trace: [Meta.debug] [‹i < a.size›, ‹j < a.size›, ‹j < b.size›]
 #guard_msgs (trace) in
 example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i ≤ j) : a[i] < a[j] + b[j] → i = j → False := by
   grind -mbtc on_failure fallback
+
+namespace Test
+
+opaque p : Prop
+axiom hp : p
+opaque h : p → Prop
+
+example : h (@Lean.Grind.nestedProof p hp) → p := by
+  grind
+
+example : h hp → p := by
+  grind
+
+end Test