Page402.mmp

$( <MM> <PROOF_ASST> THEOREM=reiteration  LOC_AFTER=
*                                                          Page402.mmp
 Press Ctrl-U to Unify this proof where we try to use
 the hypothesis directly:

h1::reiteration.1  |- ph
qed::reiteration.1 |- ph

*
 Oops, this error message is displayed:
 "E-PA-0348 Theorem reiteration Step qed: Invalid Ref = reiteration.1
 on derivation proof step. Does not specify a valid statement in the Metamath
 file that was loaded. ... Proof Text input reader last position ..."

 When you see "Proof Text input reader..." that tells you that
 the error was so severe that processing stopped immediately while
 initially examining the text. The program didn't even attempt Unification.

 The problem is that the mmj2 Proof Assistant requires that the Ref
 Label on a Derivation step refer to an Assertion, not a Hypothesis.
 This is a limitation of the mmj2 Proof Assistant, and was intended to
 simplify the programming of mmj2. In practice this isn't a significant
 limitation.

 OK, forward to the next Tutorial page (Page403.mmp)!
$)