---

Step * of Lemma l_all_cons

∀[T:Type]. ∀[P:T ⟶ ℙ].  ∀x:T. ∀L:T List.  ((∀y∈[x / L].P[y]) ⇐⇒ P[x] ∧ (∀y∈L.P[y]))
BY
{ (Auto THEN All (RWO "l_all_iff") THEN Auto) }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. x : T
4. L : T List
5. P[x]
6. ∀y:T. ((y ∈ L) ⇒ P[y])
7. y : T
8. (y ∈ [x / L])
⊢ P[y]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x:T.  \mforall{}L:T  List.    ((\mforall{}y\mmember{}[x  /  L].P[y])  \mLeftarrow{}{}\mRightarrow{}  P[x]  \mwedge{}  (\mforall{}y\mmember{}L.P[y]))


By

---

Latex:
(Auto  THEN  All  (RWO  "l\_all\_iff")  THEN  Auto)

---

Home Index