3. x2: {f:Formula| Q(f) }
4. case x1:
x
0;
p (
(p)+1);p
q ((p)+(q)+1);p
q ((p)+(q)+1);p
q ((p)+(q)+1);
5. case x2:
x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);
(x1)+(x2)+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);
(x1)+(x2)+1
| 1 | 2. x1: {f:Formula| Q(f) } 3. x2: {f:Formula| Q(f) } 4. case x1: x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);
5. case x2: x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);
(x1)+(x2)+1 |
About:
 |  |  |  |  |  |  |  |