3. y3: {f:Formula| Q(f) }
4. case y2:
x
0;
p (
(p)+1);p
q ((p)+(q)+1);p
q ((p)+(q)+1);p
q ((p)+(q)+1);
5. case y3:
x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);
(y2)+(y3)+1 
Prop
f:{f:Formula| Q(f) }.
case f:x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);
(y2)+(y3)+1
| 1 | 2. y2: {f:Formula| Q(f) } 3. y3: {f:Formula| Q(f) } 4. case y2: x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);
5. case y3: x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);
(y2)+(y3)+1 |
About:
 |  |  |  |  |  |  |  |