Step
*
1
1
1
of Lemma
hd_two_swap_permr
1. T : Type
2. as : T List
3. a : T
4. a' : T
5. ((||as|| + 1) + 1) = ((||as|| + 1) + 1) ∈ ℤ
6. i : ℕ(||as|| + 1) + 1
7. i ≠ 0
8. i = 1 ∈ ℤ
⊢ a = [a'; [a / as]][i] ∈ T
BY
{ ((RewriteWith [8] [] 0 THENM AbReduce 0) THEN Auto') }
Latex:
Latex:
1. T : Type
2. as : T List
3. a : T
4. a' : T
5. ((||as|| + 1) + 1) = ((||as|| + 1) + 1)
6. i : \mBbbN{}(||as|| + 1) + 1
7. i \mneq{} 0
8. i = 1
\mvdash{} a = [a'; [a / as]][i]
By
Latex:
((RewriteWith [8] [] 0 THENM AbReduce 0) THEN Auto')
Home
Index