Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. R:T T . (x,y:T. Dec(x R y)) (r:T T . x,y:T. (x r y) x R y)

Applied Tactic: UnivCD THENW Auto
Generated subgoals:

1. r:T T . x,y:T. (x r y) x R y