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

At: assert subst mentions trace 2 1 1
1. 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)
By: (CaseNat 0 `i') THENL [OrLeft THEN (RWO "select_cons_hd" -2);OrRight THEN (RWO "select_cons_tl" -2)]
Generated subgoal:

17. mentions_trace(2of(v[(i-1)]))
8. i = 0
subst_mentions_trace(v)

About:
productlistconsassertnatural_numberaddimpliesortrueexists

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