Level: Lib Thy Top:
Hypotheses:None
Conclusion:
S,T:
. R:S 
T 
.
(s:S. Dec(
t:T. R s t)) 
(f:{s:S| t:T. R s t} T. s:{s:S| t:T. R s t} . R s (f s))
Applied Tactic: UnivCD THENW Auto
Generated subgoals:1. f:{s:S| t:T. R s t} T. s:{s:S| t:T. R s t} . R s (f s)