Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. S:ActionSet(Alph). N:
. s:S.car.
#(S.car)=N
(A:Alph List
N < ||A||
(
a,b,c:Alph List
(0 < ||b|| 
A = (a @ b) @ c) (k:. (S:(a @ (b
k)) @ c
s) = (S:As))))
Applied Tactic: GenUnivCD THENW Auto
Generated subgoals:1. a,b,c:Alph List. (0 < ||b|| A = (a @ b) @ c) (k:. (S:(a @ (bk)) @ cs) = (S:As))