(3steps) PrintForm Definitions Lemmas mb state machine Sections GenAutomata Doc

At: kind wf2 1
1. M: sm{i:l}()
2. a: M.action

kind(a) Label & kind(a) Pattern
By: (Inst Thm* d:Decl, a:(d). kind(a) Label [M.da;a]) THENA (Try (Fold `sm_action` 0))
Generated subgoal:

13. kind(a) Label
kind(a) Pattern

About:
memberand

(3steps) PrintForm Definitions Lemmas mb state machine Sections GenAutomata Doc