Step
*
of Lemma
l_all_reverse
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀L:T List. ((∀x∈rev(L).P[x])
⇐⇒ (∀x∈L.P[x]))
BY
{ (Auto THEN (All (RWO "l_all_iff") THENA Auto) THEN RepeatFor 2 (ParallelLast)) }
1
.....antecedent.....
1. [T] : Type
2. [P] : T ⟶ ℙ
3. L : T List@i
4. ∀x:T. ((x ∈ rev(L))
⇒ P[x])
5. x : T@i
6. (x ∈ L)@i
⊢ (x ∈ rev(L))
2
.....antecedent.....
1. [T] : Type
2. [P] : T ⟶ ℙ
3. L : T List@i
4. ∀x:T. ((x ∈ L)
⇒ P[x])
5. x : T@i
6. (x ∈ rev(L))@i
⊢ (x ∈ L)
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}]. \mforall{}L:T List. ((\mforall{}x\mmember{}rev(L).P[x]) \mLeftarrow{}{}\mRightarrow{} (\mforall{}x\mmember{}L.P[x]))
By
Latex:
(Auto THEN (All (RWO "l\_all\_iff") THENA Auto) THEN RepeatFor 2 (ParallelLast))
Home
Index