is mentioned by

Thm* v:vc{i:l}(). vc_concl(v) Fmla	[vc_concl_wf]
Thm* v:vc{i:l}(). vc_hyp(v) Fmla	[vc_hyp_wf]
Def < *v* > == < v >	[vcs_singleton]
Def VCs{i} == Collection{i'}(vc{i:l}())	[vcs]

Try larger context: GenAutomata