Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
P:T
. (
x:T. Dec(P x))
Dec(
x:T.
(P x))
Dec(
x:T. P x)
Applied Tactic:
GenUnivCD THENW Auto
Generated subgoals:
1
. Dec(
x:T. P x)
T:
. P:T 
. (x:T. Dec(P x)) 
Dec(
x:T. 
(P x)) 
Dec(x:T. P x)x:T. P x)