Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

A:. L:L(A). EquivRel(A List;x,y.x Rl y)

Applied Tactic: (UnivCD THENM Unfold `equiv_rel` 0 ...a)
Generated subgoals:

1. Refl(A List;x,y.x Rl y) Sym(A List;x,y.x Rl y) Trans(A List;x,y.x Rl y)