---

Step * of Lemma l-all-iff

∀[T:Type]. ∀L:T List. ∀[P:{x:T| (x ∈ L)}  ⟶ ℙ]. (∀x∈L.P[x] ⇐⇒ (∀x∈L.P[x]))
BY
{ (Assert ⌜∀[T:Type]. ∀L:T List. ∀[P:T ⟶ ℙ]. (∀x∈L.P[x] ⇐⇒ (∀x∈L.P[x]))⌝⋅
   THEN Try (((UnivCD THENM (InstHyp [⌜{a:T| (a ∈ L)} ⌝; ⌜L⌝; ⌜P⌝] 1)⋅) THEN Auto))
   THEN (InductionOnList THENA Auto)
   THEN Unfold `l-all` 0
   THEN Reduce 0
   THEN Try (Fold `l-all` 0)
   THEN Intro
   THEN RWW "l_all_cons" 0
   THEN Auto
   THEN Try ((BackThruSomeHyp THEN Auto))
   THEN (D (-1) THEN Auto THEN BLemma `l_all_nil` THEN Auto)⋅) }

---

Latex:

---

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


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  (\mforall{}x\mmember{}L.P[x]  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x\mmember{}L.P[x]))\mkleeneclose{}\mcdot{}
  THEN  Try  (((UnivCD  THENM  (InstHyp  [\mkleeneopen{}\{a:T|  (a  \mmember{}  L)\}  \mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{};  \mkleeneopen{}P\mkleeneclose{}]  1)\mcdot{})  THEN  Auto))
  THEN  (InductionOnList  THENA  Auto)
  THEN  Unfold  `l-all`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `l-all`  0)
  THEN  Intro
  THEN  RWW  "l\_all\_cons"  0
  THEN  Auto
  THEN  Try  ((BackThruSomeHyp  THEN  Auto))
  THEN  (D  (-1)  THEN  Auto  THEN  BLemma  `l\_all\_nil`  THEN  Auto)\mcdot{})

---

Home Index