---

Step * of Lemma rel_plus_idempotent

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (R+ x y ⇐⇒ R++ x y)
BY
{ Auto }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T@i
4. y : T@i
5. R+ x y@i
⊢ R++ x y

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T@i
4. y : T@i
5. R++ x y@i
⊢ R+ x y

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y:T.    (R\msupplus{}  x  y  \mLeftarrow{}{}\mRightarrow{}  R\msupplus{}\msupplus{}  x  y)


By

---

Latex:
Auto

---

Home Index