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

At: term types closed 1
1. t: Term
2. u: TermType{i'}
3. w: t:{v:Term| u(v) }ds:Collection{i}(dec()), da1,da2:Collection{i}(SimpleType), de:sig(). closed_term(t) term_types(ds;da1;de;t) = term_types(ds;da2;de;t)
4. x: Label
5. ds: Collection{i}(dec())
6. da1: Collection{i}(SimpleType)
7. da2: Collection{i}(SimpleType)
8. de: sig()
9. closed_term(x)

da1 = da2
By:
Unfold `closed_term` -1
THEN
Reduce -1
Generated subgoal:

19. term_free_vars(x) = nil
da1 = da2

About:
setapplyfunctionuniverseimpliesall

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