Level: Lib Thy Top: 1 1
Hypotheses:

  1. S :

  2. T :

  3. R : S T

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

Conclusion:

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

Applied Tactic: D 0 THENW Auto THEN D 5 THEN Unhide THEN Auto
Generated subgoals:

None