(8steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: term subst2 mentions guard 1 1 2 2
1. as: (LabelTerm) List
2. g: Label
3. t: Term
4. u: TermType{i'}
5. w: t:{v:Term| u(v) }subst_mentions_trace(as) term_mentions_guard(g;term_subst2(as;t)) term_mentions_guard(g;t)
6. x: Label
7. i:
8. i < ||as||
9. apply_alist(as;x;x') = 2of(unzip(as))[i]

term_mentions_guard(g;2of(as[i])) mentions_trace(2of(as[i]))
By:
Auto
THEN
BackThruLemma' Thm* g:Label, t:Term. term_mentions_guard(g;t) mentions_trace(t)
Generated subgoals:

None

About:
productlistassertless_thansetapplyfunctionuniverseequalimplies

(8steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc