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