Level: Lib Thy Top: 1 1
Hypotheses:

  1. A :

  2. L : L(A)

Conclusion:

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

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

1. L (z @ a)

2. L (z @ b)