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. Type@i'
2. as 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