---

Step * of Lemma xxanti_sym_functionality_wrt_breqv

∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  uiff(anti_sym(T;R);anti_sym(T;R')) supposing R <≡>{T} R'
BY
{ ((Unfolds ``binrel_eqv xxanti_sym`` 0 
THENM RepD 
THENM RWW "-1" 0 
THENM D 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R,R':T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    uiff(anti\_sym(T;R);anti\_sym(T;R'))  supposing  R  <\mequiv{}>\{T\}  R'


By

---

Latex:
((Unfolds  ``binrel\_eqv  xxanti\_sym``  0 
THENM  RepD 
THENM  RWW  "-1"  0 
THENM  D  0)  THEN  Auto)

---

Home Index