Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
as:T List. firstn(||as||;as) = as
Applied Tactic:
(RepD ...a)
Generated subgoals:
1
. firstn(||as||;as) = as
T:
. as:T List. firstn(||as||;as) = as