(2steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

At: ioa trans all wf


A:ioa{i:l}(), I:Fmla. ioa_trans_all{i}(A;I) VCs

By: Unfolds [`vcs`;`ioa_trans_all`] 0

Generated subgoal:

11. A: ioa{i:l}()
2. I: Fmla{i}
A ioa{i':l}

About:
memberall

(2steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc