is mentioned by

Thm* t:imp{i:l}(). t.concl Fmla	[imp_concl_wf]
Thm* t:imp{i:l}(). t.hyp Fmla	[imp_hyp_wf]
Def vc{i:l}() == imp{i:l}()+qimp{i:l}()	[vc]

Try larger context: GenAutomata