scratch-notes.txt

a and b
b -> c
| ~c : assumption
| b : and e2 1
| c : -> e 2,4
| _|_ : not e 3,5
---
c : PBC 3-6

a = c
(a and b) = (d and c)
a = a : = i
(a and b) = (a and b) : = i
c = a : = e 1,3
(d and c) = (a and b) : = e 2, 4

a or b
a -> c
b -> c
| a : assumption
| c : -> e 2,4
---
| b : assumption
| c : -> e 3,6
---
c : or e 1, 4-5, 6-7

A.x(P(x) -> Q(x))
A.x(P(x))
| with x0 of x
| P(x0) -> Q(x0) : A.x e 1
| P(x0) : A.x e 2
| Q(x0) : -> e 3,4
---
A.x(Q(x)) : A.x i 3-5