Level:
Lib
Thy
Top
:
1
Hypotheses:
q :
a :
Conclusion:
l:
q List. enum(l) = a
Applied Tactic:
InstLemma `geom_series_limit` [
q
;
a
] THENA Auto THEN D 3
Generated subgoals:
1
.
l:
q List. enum(l) = a
l:q List. enum(l) = a
q
;a] THENA Auto THEN D 3 l:q List. enum(l) = a