---

Step * of Lemma refl_cl_sp_cancel

∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (dec_binrel(T;x,y:T. x = y ∈ T) ⇒ refl(T;r) ⇒ (r\\00B8) <≡>{T} r supposing anti_sym(T;r))
BY
{ ((RepD THENM AntiSymConcl) THENA Auto) }

1
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

2
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)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[r:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (dec\_binrel(T;x,y:T.  x  =  y)  {}\mRightarrow{}  refl(T;r)  {}\mRightarrow{}  (r\mbackslash{}\msupzero{})  <\mequiv{}>\{T\}  r  supposing  anti\_sym(T;r))


By

---

Latex:
((RepD  THENM  AntiSymConcl)  THENA  Auto)

---

Home Index