Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. R:Alph List 
Alph List 
. n:
.
(x:Alph List. R x x)
(x,y:Alph List. R x y 
R y x)
(x,y,z:Alph List. R x y R y z R x z)
(x,y,z:Alph List. R x y R (z @ x) (z @ y))
(
w:n Alph List. l:Alph List. i:n. R l (w i))
(a,b,c:Alph List.
||a|| 
n * n (a':Alph List. ||a'|| < ||a|| R (a @ b) (a' @ b) R (a @ c) (a' @ c)))
Applied Tactic: GenUnivCD THENW Auto THEN D 4 THEN D 5 THEN D 6 THEN D 7 THEN D 8
Generated subgoals:1. a':Alph List. ||a'|| < ||a|| R (a @ b) (a' @ b) R (a @ c) (a' @ c)