---

Step * of Lemma refl_cl_sp_le_rel

∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (refl(T;r) ⇒ ((r\\00B8) ≡>{T} r))
BY
{ ((Eval ``xxrefl refl s_part refl_cl binrel_le`` 0 
THEN RepD) THENA Auto) }

1
1. [T] : Type
2. [r] : T ⟶ T ⟶ ℙ
3. ∀a:T. (r a a)
4. x : T
5. y : T
6. (x = y ∈ T) ∨ ((r x y) ∧ (¬(r y x)))
⊢ r x y

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[r:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (refl(T;r)  {}\mRightarrow{}  ((r\mbackslash{}\msupzero{})  \mequiv{}>\{T\}  r))


By

---

Latex:
((Eval  ``xxrefl  refl  s\_part  refl\_cl  binrel\_le``  0 
THEN  RepD)  THENA  Auto)

---

Home Index