---

Step * of Lemma xxorder_functionality_wrt_breqv

∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') ⇒ (order(T;R) ⇐⇒ order(T;R')))
BY
{ Auto }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [R'] : T ⟶ T ⟶ ℙ
4. R <≡>{T} R'@i
5. order(T;R)@i
⊢ order(T;R')

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [R'] : T ⟶ T ⟶ ℙ
4. R <≡>{T} R'@i
5. order(T;R')@i
⊢ order(T;R)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R,R':T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    ((R  <\mequiv{}>\{T\}  R')  {}\mRightarrow{}  (order(T;R)  \mLeftarrow{}{}\mRightarrow{}  order(T;R')))


By

---

Latex:
Auto

---

Home Index