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]
Thm* p:Fmla, x:Label. pred_mentions(p;x) Prop	[pred_mentions_wf]
Thm* t:qimp{i:l}(). t.concl Fmla	[qimp_concl_wf]
Thm* t:qimp{i:l}(). t.hyp Fmla	[qimp_hyp_wf]
Thm* t:imp{i:l}(). t.concl Fmla	[imp_concl_wf]
Thm* t:imp{i:l}(). t.hyp Fmla	[imp_hyp_wf]
Def qimp{i:l}() == LabelFmlaFmla	[qimp]
Def imp{i:l}() == FmlaFmla	[imp]

Try larger context: GenAutomata