is mentioned by

Thm* t:Term, e,s,s',a1,a2,tr:Top. closed_term(t) ([[t]] e s s' a1 tr ~ [[t]] e s s' a2 tr)	[closed_term_mng2]
Thm* t:Term, e,s,a1,a2,tr:Top. closed_term(t) ([[t]] e s a1 tr ~ [[t]] e s a2 tr)	[closed_term_mng]
Thm* t1,t2:Term. closed_term(t1 t2) closed_term(t1) & closed_term(t2)	[closed_tapp]

Try larger context: GenAutomata