Step
*
1
1
of Lemma
select_append_back
1. T : Type
2. bs : T List
3. i : ℕ0 + ||bs||
⊢ bs[i] = bs[i - 0] ∈ T
BY
{ Auto }
Latex:
Latex:
1. T : Type
2. bs : T List
3. i : \mBbbN{}0 + ||bs||
\mvdash{} bs[i] = bs[i - 0]
By
Latex:
Auto
Home
Index