PrintForm Definitions mb automata 4 Sections GenAutomata Doc

At: smts eff pred wf

p:Fmla, ss:Collection(smt()). smts_eff_pred(ss;p) Fmla
By:
Unfolds [`pred`;`smts_eff_pred`] 0
THEN
Fold `pred` 0
Generated subgoals:

None

About:
memberall

PrintForm Definitions mb automata 4 Sections GenAutomata Doc