(2steps) PrintForm Definitions mb state machine Sections GenAutomata Doc

At: small action

I:Type, M:(Ism{i:l}()), j:I, x:i:IM(i).action. x M(j).action
By:
Unfolds [`sm_all`;`sm_action`] 0
THEN
Reduce 0
Generated subgoal:

11. I: Type
2. M: Ism{i:l}()
3. j: I
4. x: ((M(i)).da for i I)
x ((M(j)).da)

About:
applyfunctionuniversememberall

(2steps) PrintForm Definitions mb state machine Sections GenAutomata Doc