Level: Lib Thy Top: 1 1
Hypotheses:

  1. A :

  2. L : L(A)

Conclusion:

a,z:A List. L (z @ a) L (z @ a)

Applied Tactic: (Unfold `languages` 2 ...)
Generated subgoals:

None