is mentioned by

Thm* r:rel(), as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) rel_subst2(as;(r)') = rel_subst(as;r)	[rel_subst2_addprime]
Thm* x:Term, as:(LabelTerm) List. (v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x)	[term_subst2_addprime]
Def t.hyp == 1of(2of(t))	[qimp_hyp]
Def t.lbl == 1of(t)	[qimp_lbl]
Def t.hyp == 1of(t)	[imp_hyp]

In prior sections: core mb list 1 mb automata 1 prog 1 mb record

Try larger context: GenAutomata