PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: switch inv wf

E:TaggedEventStruct. switch_inv(E) (|E| List)Prop
By:
Auto
THEN
AssertBY (E EventStruct) ((BackThru Thm* E:TaggedEventStruct. E EventStruct) THEN Trivial)
THEN
Unfold `switch_inv` 0
Generated subgoals:

None

About:
listfunctionmemberpropall

PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc