Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
equiv:{T
}.
eq:{T=
}.
u:T.
L:T List.
u(
eq) L
(
v:T.
(equiv u v)
v(
equiv) L)
Applied Tactic:
Fiat
Generated subgoals:
None
T:
. equiv:{T
}. eq:{T=}. u:T. L:T List. 
u(
eq) L 
(v:T. (equiv u v) v(equiv) L)