---

Step * of Lemma l_all2_cons

∀[T:Type]. ∀L:T List. ∀[P:T ⟶ T ⟶ ℙ]. ∀u:T. ((∀x<y∈[u / L].P[x;y]) ⇐⇒ (∀y∈L.P[u;y]) ∧ (∀x<y∈L.P[x;y]))
BY
{ ((UnivCD THENA Auto)
   THEN Unfolds ``l_all2`` 0
   THEN RWO "l_all_iff cons_before" 0
   THEN Auto
   THEN skip{(Try (Complete ((BackThruSomeHyp THEN Auto THEN SimpConcl))) THEN (D (-1)) THEN EasyHyp)}) }

1
1. [T] : Type
2. L : T List
3. [P] : T ⟶ T ⟶ ℙ
4. u : T
5. ∀y:T. ((y ∈ L) ⇒ P[u;y])
6. ∀x,y:T.  (x before y ∈ L ⇒ P[x;y])
7. x : T
8. y : T
9. ((x = u ∈ T) ∧ (y ∈ L)) ∨ x before y ∈ L
⊢ P[x;y]

---

Latex:

---

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


By

---

Latex:
...

---

Home Index