Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. S :

  3. T1 :

  4. f : T S

  5. g : T S

  6. T1 T

  7. f = g

Conclusion:

f = g

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

1. f x = g x