Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T,Z:. P:T Z . (x:T. y:Z. Dec(P[x;y])) (f_p:T Z . x:T. y:Z. P[x;y] (f_p x y))

Applied Tactic: UnivCD THENA Auto
Generated subgoals:

1. f_p:T Z . x:T. y:Z. P[x;y] (f_p x y)