Assignment VI:

Prove the following two theorems.  They are both theorems we proved using
natural deduction in class.

(* the first example *)

Start "(Ax1.(Ax2.x1 R1 x2 -> x2 R1 x1)) & (Ax1.(Ax2.(Ax3.x1 R1 x2 & x2 R1 x3 -> x1 R1 x3))) & (Ax1.(Ex2.x1 R1 x2)) -> (Ax1.x1 R1 x1)";

(* the second main example we did in class *)

s "(Ax1.(Ex2.x1 R2 x2)) & (Ex1.(Ax2.P1(x2)v x1 R2 x2)) & (Ax1.(Ax2.(x1 R2 x2 & P1(x1) ->  x2 R2 x1))) -> (Ax1.(Ex2.x2 R2 x1))";

For four of the examples in Assignment V, prove them and set up the proofs
in tree form.  Something like P(x) & Q(y) can be set up as P1(x1) & P2(x2);
something like (Ex.A(x)->B) sets up as (Ex1.P1(x1)->P2)