---

Step * of Lemma bm_compare_sym_eq

∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K].  (((compare k1 k2) = 0 ∈ ℤ) ⇒ ((compare k2 k1) = 0 ∈ ℤ))
BY
{ (Auto THEN Unfold `bm_compare` 2 THEN DVarSets THEN Auto) }

---

Latex:


\mforall{}[K:Type].  \mforall{}[compare:bm\_compare(K)].  \mforall{}[k1,k2:K].    (((compare  k1  k2)  =  0)  {}\mRightarrow{}  ((compare  k2  k1)  =  0))


By

(Auto  THEN  Unfold  `bm\_compare`  2  THEN  DVarSets  THEN  Auto)

---

Home Index