Step
*
of Lemma
iseg-iff-firstn
∀[T:Type]. ∀L1,L2:T List. (L1 ≤ L2
⇐⇒ (||L1|| ≤ ||L2||) ∧ (L1 = firstn(||L1||;L2) ∈ (T List)))
BY
{ ((UnivCD THENA Auto) THEN RWO "firstn_is_iseg" 0 THEN Auto THEN ExRepD) }
1
1. T : Type
2. L1 : T List
3. L2 : T List
4. n : ℕ||L2|| + 1
5. L1 = firstn(n;L2) ∈ (T List)
⊢ ||L1|| ≤ ||L2||
2
1. T : Type
2. L1 : T List
3. L2 : T List
4. n : ℕ||L2|| + 1
5. L1 = firstn(n;L2) ∈ (T List)
⊢ L1 = firstn(||L1||;L2) ∈ (T List)
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}L1,L2:T List. (L1 \mleq{} L2 \mLeftarrow{}{}\mRightarrow{} (||L1|| \mleq{} ||L2||) \mwedge{} (L1 = firstn(||L1||;L2)))
By
Latex:
((UnivCD THENA Auto) THEN RWO "firstn\_is\_iseg" 0 THEN Auto THEN ExRepD)
Home
Index