proof instance : (!x:t.P(x)) => (?y:t.T) => (?z:t.P(z)) = begin [ !x:t.P(x); [ ?y:t.T; [ y:t, T; P(y); ?z:t.P(z) ]; ?z:t.P(z) ]; (?y:t.T) => (?z:t.P(z)) ]; (!x:t.P(x)) => (?y:t.T) => (?z:t.P(z)) end; proof dm : (!x:t.~P(x)) => ~(?x:t.P(x)) = begin [ !x:t.~P(x); [ ?x:t.P(x); [ y:t, P(y); ~P(y); F ]; F ]; ~(?x:t.P(x)) ]; (!x:t.~P(x)) => ~(?x:t.P(x)) end; proof eximp : (?x:t.P(x) => Q(x)) => (!x:t.P(x)) => (?x:t.Q(x)) = begin [ ?x:t.P(x) => Q(x); [ !x:t.P(x); [ y:t, P(y) => Q(y); P(y); Q(y); ?x:t.Q(x) ]; ?x:t.Q(x); ]; (!x:t.P(x)) => (?x:t.Q(x)) ]; (?x:t.P(x) => Q(x)) => (!x:t.P(x)) => (?x:t.Q(x)) end; proof allor : ((!x:t. P(x)) | (!x:t. Q(x))) => !x:t. P(x) | Q(x) = begin [ (!x:t. P(x)) | (!x:t. Q(x)); [ y:t; [ !x:t. P(x); P(y); P(y) | Q(y) ]; [ !x:t. Q(x); Q(y); P(y) | Q(y) ]; P(y) | Q(y) ]; !x:t. P(x) | Q(x) ]; ((!x:t. P(x)) | (!x:t. Q(x))) => !x:t. P(x) | Q(x) end; proof spread : (?x:t.P(x)) => (!x:t.!y:t.P(x) => P(y)) => !x:t.P(x) = begin [ ?x:t.P(x); [ !x:t.!y:t. P(x) => P(y); [ z:t, P(z); [ w:t; !y:t. P(z) => P(y); P(z) => P(w); P(w) ]; !x:t.P(x) ]; !x:t.P(x) ]; (!x:t.!y:t. P(x) => P(y)) => !x:t.P(x) ]; (?x:t.P(x)) => (!x:t.!y:t. P(x) => P(y)) => !x:t.P(x) end;