---

Step * of Lemma lg-all_functionality

∀[T:Type]. ∀G:LabeledDAG(T). ∀[P1,P2:T ⟶ ℙ].  ((∀x:T. (P1[x] ⇒ P2[x])) ⇒ {∀x∈G.P1[x] ⇒ ∀x∈G.P2[x]})
BY
{ (Unfold `guard` 0
   THEN (RepeatFor 2 ((D 0 THENA Auto))
         THEN D -1
         THEN Auto
         THEN RepeatFor 2 (ParallelLast)
         THEN BHyp 6 
         THEN Try (Complete (Auto)))
   ) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}G:LabeledDAG(T).  \mforall{}[P1,P2:T  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:T.  (P1[x]  {}\mRightarrow{}  P2[x]))  {}\mRightarrow{}  \{\mforall{}x\mmember{}G.P1[x]  {}\mRightarrow{}  \mforall{}x\mmember{}G.P2[x]\})


By

---

Latex:
(Unfold  `guard`  0
  THEN  (RepeatFor  2  ((D  0  THENA  Auto))
              THEN  D  -1
              THEN  Auto
              THEN  RepeatFor  2  (ParallelLast)
              THEN  BHyp  6 
              THEN  Try  (Complete  (Auto)))
  )

---

Home Index