Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. P : T

  3. (x:T. Dec(P x)) Dec(x:T. (P x))

Conclusion:

Dec(x:T. P x)

Applied Tactic: D 3
Generated subgoals:

1. Dec(x:T. P x)