PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: dec lookup monotone

x:Label, a1,a2:Collection(dec()). a1 a2 dec_lookup(a1;x) dec_lookup(a2;x)
By:
Unfold `col_le` 0
THEN
RWW "member_dec_lookup" 0
THEN
BackThruSomeHyp
Generated subgoals:

None

About:
impliesall

PrintForm Definitions mb automata 2 Sections GenAutomata Doc