Nuprl - Pf fimp wf

At: fimp wf

p,q:Formula. pq Formula

By: UnivCD THEN Unfold `fimp` 0

Generated subgoal:

1 1. p: Formula
2. q: Formula
inr(inr(inr(inr( < p,q > )))) Formula

About: