---

Step * of Lemma xxtrans_imp_sp_trans

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (trans(T;R) ⇒ trans(T;R\))
BY
{ AssertLemma `trans_imp_sp_trans` [] }

1
1. ∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (Trans(T;a,b.R[a;b]) ⇒ Trans(T;a,b.strict_part(x,y.R[x;y];a;b)))
⊢ ∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (trans(T;R) ⇒ trans(T;R\))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (trans(T;R)  {}\mRightarrow{}  trans(T;R\mbackslash{}))


By

---

Latex:
AssertLemma  `trans\_imp\_sp\_trans`  []

---

Home Index