---

Step * of Lemma l_all_append

∀[T:Type]. ∀[P:T ⟶ ℙ].  ∀L1,L2:T List.  ((∀x∈L1 @ L2.P[x]) ⇐⇒ (∀x∈L1.P[x]) ∧ (∀x∈L2.P[x]))
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "l_all_iff" 0 THEN Auto)
   THEN Try ((((RWO "member_append" (-1)) THENA Auto{1,4}-1) THEN (D (-1)) THEN EasyHyp))
   THEN BackThruSomeHyp
   THEN Try (((RWO "member_append" 0 THENA Auto{1,4}-1) THEN SimpConcl))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}L1,L2:T  List.    ((\mforall{}x\mmember{}L1  @  L2.P[x])  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x\mmember{}L1.P[x])  \mwedge{}  (\mforall{}x\mmember{}L2.P[x]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "l\_all\_iff"  0  THEN  Auto)
  THEN  Try  ((((RWO  "member\_append"  (-1))  THENA  Auto\{1,4\}-1)  THEN  (D  (-1))  THEN  EasyHyp))
  THEN  BackThruSomeHyp
  THEN  Try  (((RWO  "member\_append"  0  THENA  Auto\{1,4\}-1)  THEN  SimpConcl)))

---

Home Index