---

Step * of Lemma decidable__dstype_equal

∀[A:Type]. ∀a:A. ∀d:DS(A). ∀x,y:dstype(A; d; a).  Dec(x = y ∈ dstype(A; d; a))
BY
{ (Unfolds ``discrete_struct dstype`` 0
   THEN Auto
   THEN D 3
   THEN All Reduce
   THEN Auto
   THEN GenConclTerm ⌜d1 a⌝⋅
   THEN Auto
   THEN (Thin (-1))) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}a:A.  \mforall{}d:DS(A).  \mforall{}x,y:dstype(A;  d;  a).    Dec(x  =  y)


By

---

Latex:
(Unfolds  ``discrete\_struct  dstype``  0
  THEN  Auto
  THEN  D  3
  THEN  All  Reduce
  THEN  Auto
  THEN  GenConclTerm  \mkleeneopen{}d1  a\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (Thin  (-1)))

---

Home Index