Incorrect proof status for steps

[expln]

1. Load:
   1.1 set.mm, stop before mathbox;
   1.2 my-new-theorems.mm, read all (see the content of my-new-theorems.mm below).
2. Import from JSON:

{"srcs":[{"typ":"Local","fileName":"set.mm","url":"","readInstr":"StopBefore","label":"mathbox","resetNestingLevel":true,"allLabels":[]},{"typ":"Local","fileName":"my-new-theorems.mm","url":"","readInstr":"ReadAll","label":"","resetNestingLevel":true,"allLabels":[]}],"descr":"","varsText":"","disjText":"A x","stmts":[{"label":"2","typ":"p","isGoal":false,"isBkm":false,"cont":"|- A e. { A , B }","jstfText":""},{"label":"4","typ":"p","isGoal":false,"isBkm":false,"cont":"|- A e. { x e. RR | ( F ` x ) = 4 }","jstfText":""},{"label":"5","typ":"p","isGoal":false,"isBkm":false,"cont":"|- F/_ x A","jstfText":": nfcv"},{"label":"6","typ":"p","isGoal":false,"isBkm":false,"cont":"|- F/_ x RR","jstfText":": nfcv"},{"label":"8","typ":"p","isGoal":false,"isBkm":false,"cont":"|- F/_ x ( x e. RR |-> ( ( ( K x. ( x ^ 2 ) ) - ( ( 2 x. K ) x. x ) ) + L ) )","jstfText":": nfmpt1"},{"label":"9","typ":"p","isGoal":false,"isBkm":false,"cont":"|- F/_ x F","jstfText":""},{"label":"10","typ":"p","isGoal":false,"isBkm":false,"cont":"|- F/_ x ( F ` A )","jstfText":"9 5 : nffv"},{"label":"11","typ":"p","isGoal":false,"isBkm":false,"cont":"|- F/ x ( F ` A ) = 4","jstfText":"10 : nfeq1"},{"label":"12","typ":"p","isGoal":false,"isBkm":false,"cont":"|- ( x = A -> ( ( F ` x ) = 4 <-> ( F ` A ) = 4 ) )","jstfText":": fveqeq2"},{"label":"13","typ":"p","isGoal":false,"isBkm":false,"cont":"|- ( A e. { x e. RR | ( F ` x ) = 4 } <-> ( A e. RR /\\ ( F ` A ) = 4 ) )","jstfText":"5 6 11 12 : elrabf"},{"label":"14","typ":"p","isGoal":false,"isBkm":false,"cont":"|- ( A e. RR /\\ ( F ` A ) = 4 )","jstfText":"4 13 : mpbi"},{"label":"simp_problem_lem_1","typ":"p","isGoal":true,"isBkm":false,"cont":"|- ( F ` A ) = 4","jstfText":"14 : simpri"}]}

3. Unify all.

Expected: All steps are marked as proved.
Actual: The step 10 is marked as proved. However, it depends on the step 9, which is marked as unproved.

The content of my-new-theorems.mm:

$[ set.mm $]

simp_problem_hyp_1 $e |- K e. _V $.
simp_problem_hyp_2 $e |- L e. _V $.
simp_problem_hyp_3 $e |- A e. _V $.
simp_problem_hyp_4 $e |- B e. _V $.
simp_problem_hyp_5 $e |- 0 < K $.
simp_problem_hyp_6 $e |- 0 < L $.
simp_problem_hyp_7 $e |- F = ( x e. RR |-> ( ( ( K x. ( x ^ 2 ) ) - ( ( 2 x. K ) x. x ) ) + L ) ) $.
simp_problem_hyp_8 $e |- { x e. RR | ( F ` x ) = 4 } = { A , B } $.
simp_problem_hyp_9 $e |- ( ( ( A - B ) ^ 2 ) + ( ( ( F ` A ) - ( F ` B ) ) ^ 2 ) ) = ( 6 ^ 2 ) $.
simp_problem_hyp_10 $e |- ( ( ( A ^ 2 ) + ( ( F ` A ) ^ 2 ) ) + ( ( B ^ 2 ) + ( ( F ` B ) ^ 2 ) ) ) = C $.