citp describe

:describe proof

Describes the current proof in more detail.

Related: :show, citp

Example

PNAT> :describe proof
==> root*
    -- context module: #Goal-root
    -- targeted sentences:
      eq [lemma-1]: M:PNat + 0 = M .
      eq [lemma-2]: M:PNat + s N:PNat = s (M + N) .
[si]    1*
    -- context module: #Goal-1
    -- targeted sentences:
      eq [lemma-1]: 0 + 0 = 0 .
      eq [lemma-2]: 0 + s N:PNat = s (0 + N) .
...