Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
E,T,L:
.
S:Signature(E;T;L).
L
L
Applied Tactic:
Unfold `sign_l_ref_rel` 0 THEN Auto
Generated subgoals:
None