Level: Lib Thy Top: 1 1
Hypotheses:

  1. T :

  2. f : T

  3. t:T. Dec(f t)

Conclusion:

x:T. y:. f x y

Applied Tactic: D 0 THENW Auto
Generated subgoals:

1. y:. f x y