---

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