---

Step * 1 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\\00B8) ≡>{T} r
BY
{ ((BLemma `refl_cl_sp_le_rel`) 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\mbackslash{}\msupzero{})  \mequiv{}>\{T\}  r


By

---

Latex:
((BLemma  `refl\_cl\_sp\_le\_rel`)  THEN  Auto)

---

Home Index