---

Step * of Lemma as_strong_transitivity

∀[T:Type]. ∀[P,Q,R:T ⟶ ℙ].  (P as strong as Q  ⇒ Q as strong as R  ⇒ P as strong as R )
BY
{ (((Unfold `as_strong` 0 THEN Auto) THEN Assert Q x) THEN EasyHyp) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P,Q,R:T  {}\mrightarrow{}  \mBbbP{}].    (P  as  strong  as  Q    {}\mRightarrow{}  Q  as  strong  as  R    {}\mRightarrow{}  P  as  strong  as  R  )


By

---

Latex:
(((Unfold  `as\_strong`  0  THEN  Auto)  THEN  Assert  Q  x)  THEN  EasyHyp)

---

Home Index