Goal: (<E'> o Reverse(Q')) = Reverse(Q)
	Q – the original Q
	Q' – what was given to Flip
	E' – item that was dequeued

Given:
1.	(min_int <= 0)
2.	(0 < max_int)
3.	(Last_Char_Num > 0)
4.	(Max_Length > 0)
5.	(min_int <= Max_Length) and (Max_Length <= max_int)
6.	(|Q| <= Max_Length)
7.	P_val = |Q|
8.	|Q| /= 0
9.	Q = (<E'> o Q')


Above, I've copied the Goal and Givens from the RESOLVE Web Interface.
Below I copied the Goal from above and proceeded to use Given #9 to make
the right hand side of the goal look like the left hand side.
The proof fails because the implementation for Invert calls Inject which
puts the item onto the front of the queue. Invert should have called
Enqueue to put the item onto the rear of the queue. 

So what the failed proof shows on line S3, on the right hand side is that the
Goal indicates that E' should be enqueued (onto the right end), but the
code injects it onto the front end (this is the left hand side of the S3).


Goal: (<E'> o Reverse(Q')) = Reverse(Q)
S1. (<E'> o Reverse(Q')) = Reverse(<E'> o Q')
S2. (<E'> o Reverse(Q')) = Reverse(Q') o Reverse(<E'>)
S3. (<E'> o Reverse(Q')) = Reverse(Q') o <E'>