Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

Alph:. S:ActionSet(Alph). s:S.car. L1,L2,L:Alph List. (S:L1s) = (S:L2s) (S:L @ L1s) = (S:L @ L2s)

Applied Tactic: UnivCD THENW Auto
Generated subgoals:

1. (S:L @ L1s) = (S:L @ L2s)