Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T,S,T1:. f,g:T S. T1 T f = g f = g

Applied Tactic: (UnivCD ...a)
Generated subgoals:

1. f = g