Step
*
of Lemma
whole_segment
∀T:Type. ∀as:T List. ((as[0..||as||-]) = as ∈ (T List))
BY
{ ((RepD THENM RWO "segment_factor" 0) THENA Auto{2,3}-1') }
1
1. T : Type@i'
2. as : T List@i
⊢ (Π 0 ≤ k < ||as||. [as[k]]) = as ∈ (T List)
Latex:
Latex:
\mforall{}T:Type. \mforall{}as:T List. ((as[0..||as||\msupminus{}]) = as)
By
Latex:
((RepD THENM RWO "segment\_factor" 0) THENA Auto\{2,3\}-1')
Home
Index