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

At: closed term mng 2

1. t: Term
2. u: TermType{i'}
3. w: t:{v:Term| u(v) }e,s,a1,a2,tr:Top. closed_term(t) ([[t]] e s a1 tr ~ [[t]] e s a2 tr)
4. y1: {v:Term| u(v) }
5. y2: {v:Term| u(v) }
6. e: Top
7. s: Top
8. a1: Top
9. a2: Top
10. tr: Top
11. closed_term(y1 y2)

([[y1]] e s a1 tr([[y2]] e s a1 tr)) ~ ([[y1]] e s a2 tr([[y2]] e s a2 tr))

By:
RWW "closed_tapp" -1
THEN
Analyze
THEN
BackThruSomeHyp


Generated subgoals:

None

About:
setapplyfunctionuniversesqequaltopimpliesall

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