Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. equiv:{T}. eq:{T=}. u:T. L:T List. u(equiv) L (v:T. (equiv u v) v(eq) L)

Applied Tactic: UnivCD THENA Auto
Generated subgoals:

1. v:T. (equiv u v) v(eq) L