x1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x1])
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