Level: Lib Thy Top: 1
Hypotheses:

  1. S :

  2. T :

  3. R : S T

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

Conclusion:

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

Applied Tactic: InstLemma `ax_choice` [{s:S| t:T. R s t} ;T;x y.R x y] THENW Auto
Generated subgoals:

1. x:{s:S| t:T. R s t} . y:T. R x y

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