Level: Lib Thy Top: 1
Hypotheses:

  1. A :

  2. L : L(A)

Conclusion:

Sym(A List;x,y.x Rl y)

Applied Tactic: (Unfolds ``sym lang_rel`` 0 THENM Reduce 0 ...a)
Generated subgoals:

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