Level: Lib Thy Top: 1 2
Hypotheses:

  1. S :

  2. T :

  3. R : S T

  4. s:S. Dec(t:T. R s t)

  5. f:{s:S| t:T. R s t} T. x:{s:S| t:T. R s t} . R x (f x)

Conclusion:

f:{s:S| t:T. R s t} T. s:{s:S| t:T. R s t} . R s (f s)

Applied Tactic: Auto
Generated subgoals:

None