---

Step * of Lemma l_all-cons

∀[T:Type]. ∀x:T. ∀L:T List.  ∀[P:{a:T| (a ∈ [x / L])}  ⟶ ℙ]. ((∀a∈[x / L].P[a]) ⇐⇒ P[x] ∧ (∀a∈L.P[a]))
BY
{ ((UnivCD THENA Auto)
   THEN InstLemma `l_all_cons` [⌜{a:T| (a ∈ [x / L])} ⌝;⌜P⌝;⌜x⌝;⌜L⌝]⋅
   THEN Auto
   THEN SubsumeC ⌜{a:T| (a ∈ L)}  List⌝⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  InstLemma  `l\_all\_cons`  [\mkleeneopen{}\{a:T|  (a  \mmember{}  [x  /  L])\}  \mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  SubsumeC  \mkleeneopen{}\{a:T|  (a  \mmember{}  L)\}    List\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index