---

Step * 2 of Lemma refl_cl_sp_cancel


1. [T] : Type
2. [r] : T ⟶ T ⟶ ℙ
3. dec_binrel(T;x,y:T. x = y ∈ T)@i
4. refl(T;r)@i
5. anti_sym(T;r)
⊢ r ≡>{T} (r\\00B8)
BY
{ ((BLemma `rel_le_refl_cl_sp`) THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [r]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  dec\_binrel(T;x,y:T.  x  =  y)@i
4.  refl(T;r)@i
5.  anti\_sym(T;r)
\mvdash{}  r  \mequiv{}>\{T\}  (r\mbackslash{}\msupzero{})


By

---

Latex:
((BLemma  `rel\_le\_refl\_cl\_sp`)  THEN  Auto)

---

Home Index