---

Step * 1 of Lemma xxtrans_imp_sp_trans


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\))
BY
{ Unfolds ``strict_part so_apply`` 1  
THEN Unfolds ``xxtrans s_part`` 0 
THEN Reduce 0  
THEN Trivial }

---

Latex:

---

Latex:

1.  \mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (Trans(T;a,b.R[a;b])  {}\mRightarrow{}  Trans(T;a,b.strict\_part(x,y.R[x;y];a;b)))
\mvdash{}  \mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (trans(T;R)  {}\mRightarrow{}  trans(T;R\mbackslash{}))


By

---

Latex:
Unfolds  ``strict\_part  so\_apply``  1   
THEN  Unfolds  ``xxtrans  s\_part``  0 
THEN  Reduce  0   
THEN  Trivial

---

Home Index