Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T,U:. P:T U . (x:T. y:U. Dec(P[x;y])) (p:T U. Dec(let <l,r> = p in P[l;r]))

Applied Tactic: UnivCD THENA Auto
Generated subgoals:

1. Dec(let <l,r> = p in P[l;r])