Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
(
Alph,S,L,s,z.(S:L
s))
Alph:
S:ActionSet(Alph)
L:Alph List
s:S.car
True
S.car
Applied Tactic:
ProveOpCombTyping `maction_wf`
Generated subgoals:
None
(
Alph,S,L,s,z.(S:L
s)) 
Alph:
S:ActionSet(Alph) L:Alph List s:S.car 
True S.car