---

Step * of Lemma restriction-of-transitive

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ].  (Trans(T;x,y.R x y) ⇒ Trans(T;x,y.R|P x y))
BY
{ Auto }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [P] : T ⟶ ℙ
4. Trans(T;x,y.R x y)@i
⊢ Trans(T;x,y.R|P x y)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    (Trans(T;x,y.R  x  y)  {}\mRightarrow{}  Trans(T;x,y.R|P  x  y))


By

---

Latex:
Auto

---

Home Index