PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: term types monotone member

ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), t:Term. ds1 ds2 da1 da2 (a:SimpleType. a term_types(ds1;da1;de;t) a term_types(ds2;da2;de;t))
By:
Fold `col_le` 0
THEN
BackThru Thm* ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType) , de:sig(), t:Term. ds1 ds2 da1 da2 term_types(ds1;da1;de;t) term_types(ds2;da2;de;t)
Generated subgoals:

None

About:
impliesall

PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc