Step
*
1
of Lemma
itop_aux_wf
1. A : Type
2. op : A ⟶ A ⟶ A
3. id : A
4. p : ℤ
5. q : {p...}
6. E : {p..q-} ⟶ A
⊢ Π(op,id) p ≤ i < q. E[i] ∈ A
BY
{ (MoveToConcl (-1) THEN RankInd λx.(x - p) 5 ⋅ THEN Auto) }
Latex:
Latex:
1. A : Type
2. op : A {}\mrightarrow{} A {}\mrightarrow{} A
3. id : A
4. p : \mBbbZ{}
5. q : \{p...\}
6. E : \{p..q\msupminus{}\} {}\mrightarrow{} A
\mvdash{} \mPi{}(op,id) p \mleq{} i < q. E[i] \mmember{} A
By
Latex:
(MoveToConcl (-1) THEN RankInd \mlambda{}x.(x - p) 5 \mcdot{} THEN Auto)
Home
Index