Step
*
2
of Lemma
vdf-eq-firstn
1. A : Type
2. f : Top
3. L : (a:Top × b:Top × Top) List
4. i : ℕ||L||
5. ¬i + 1 < 1
6. @0 : Base
⊢ let a,b,c = firstn(i + 1;L)[i] in
a = (f firstn(i;firstn(i + 1;L)) b) ∈ A ~ (fst(L[i])) = (f firstn(i;L) (fst(snd(L[i])))) ∈ A
BY
{ ((RWO "select-firstn firstn-firstn" 0 THENA Auto)
THEN (GenConclTerm ⌜L[i]⌝⋅ THENA Auto)
THEN RepeatFor 2 (D -2)
THEN Reduce 0
THEN Auto) }
Latex:
Latex:
1. A : Type
2. f : Top
3. L : (a:Top \mtimes{} b:Top \mtimes{} Top) List
4. i : \mBbbN{}||L||
5. \mneg{}i + 1 < 1
6. @0 : Base
\mvdash{} let a,b,c = firstn(i + 1;L)[i] in
a = (f firstn(i;firstn(i + 1;L)) b) \msim{} (fst(L[i])) = (f firstn(i;L) (fst(snd(L[i]))))
By
Latex:
((RWO "select-firstn firstn-firstn" 0 THENA Auto)
THEN (GenConclTerm \mkleeneopen{}L[i]\mkleeneclose{}\mcdot{} THENA Auto)
THEN RepeatFor 2 (D -2)
THEN Reduce 0
THEN Auto)
Home
Index