(4steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: term primed vars term vars 2

1. x: Label
2. u: Term
3. u1: TermType{i'}
4. w: u:{v:Term| u1(v) }(x term_primed_vars(u)) (x term_vars(u))
5. y1: {v:Term| u1(v) }
6. y2: {v:Term| u1(v) }
7. (x term_primed_vars(y1) @ term_primed_vars(y2))

(x term_vars(y1) @ term_vars(y2))

By: All (RWO "member_append")

Generated subgoal:

17. (x term_primed_vars(y1)) (x term_primed_vars(y2))
(x term_vars(y1)) (x term_vars(y2))

About:
setapplyfunctionuniverseimpliesor

(4steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc