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

At: assert subst mentions trace

as:(LabelTerm) List. subst_mentions_trace(as) (i:||as||. mentions_trace(2of(as[i])))
By:
InductionOnList
THEN
Reduce 0
Generated subgoals:

11. as: (LabelTerm) List
subst_mentions_trace(nil) (i:0. mentions_trace(2of(nil[i])))
21. as: (LabelTerm) List
2. u: LabelTerm
3. v: (LabelTerm) List
4. subst_mentions_trace(v) (i:||v||. mentions_trace(2of(v[i])))
subst_mentions_trace([u / v]) (i:(||v||+1). mentions_trace(2of([u / v][i])))

About:
productlistconsnilassertnatural_numberaddallexists

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