mb automata 2 Sections GenAutomata Doc

Def Case vc_imp(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z))

is mentioned by

Def vc_concl(v) == Case(v) Case vc_imp(x) = > x.concl Case vc_qimp(x) = > x.concl Default = > False[vc_concl]
Def vc_hyp(v) == Case(v) Case vc_imp(x) = > x.hyp Case vc_qimp(x) = > x.hyp Default = > False[vc_hyp]

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc