(6steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: assert subst mentions trace 1
1. as: (LabelTerm) List

subst_mentions_trace(nil) (i:0. mentions_trace(2of(nil[i])))
By:
Unfold `subst_mentions_trace` 0
THEN
Reduce 0
THEN
ExRepD
Generated subgoals:

None

About:
productlistnilassertnatural_numberexists

(6steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc