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

At: assert subst mentions trace 2 1
1. as: (LabelTerm) List
2. u: LabelTerm
3. v: (LabelTerm) List
4. subst_mentions_trace(v) (i:||v||. mentions_trace(2of(v[i])))

mentions_trace(2of(u)) subst_mentions_trace(v) (i:(||v||+1). mentions_trace(2of([u / v][i])))
By:
Auto
THEN
Analyze -1
THEN
AllHyps SimpHyp
THEN
Try ((InstConcl [0]) THEN (Reduce 0) THEN (Complete Auto))
THEN
Try (ExRepD THEN (InstConcl [i+1]) THEN (RW SelectConsC 0))
Generated subgoal:

11. True
2. u: LabelTerm
3. v: (LabelTerm) List
4. subst_mentions_trace(v) (i:||v||. mentions_trace(2of(v[i])))
5. subst_mentions_trace(v) (i:||v||. mentions_trace(2of(v[i])))
6. i: (||v||+1)
7. mentions_trace(2of([u / v][i]))
mentions_trace(2of(u)) subst_mentions_trace(v)

About:
productlistconsassertnatural_numberaddorexists

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