Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
E,T,L:
.
s:Signature(E;T;L). <
T
T
Applied Tactic:
ModulePiTac 10 ``sign_e_rel sign_t_rel sign_l_rel sign_inst_e sign_time sign_d sign_t0 sign_t1 sign_ def_t sign_def_l``
Generated subgoals:
None
E,T,L:
. s:Signature(E;T;L). < 
T 
T 