---

Step * of Lemma decidable__equal_MaName

∀x,y:MaName.  Dec(x = y ∈ MaName)
BY
{ (((InstLemma `deq_property` [⌈MaName⌉; ⌈maname-deq()⌉])⋅ THENA Auto) THEN RepeatFor 2 (ParallelLast)) }

1
1. ∀[x,y:MaName].  uiff(x = y ∈ MaName;↑(maname-deq() x y))
2. x : MaName@i
3. ∀[y:MaName]. uiff(x = y ∈ MaName;↑(maname-deq() x y))
4. y : MaName@i
5. uiff(x = y ∈ MaName;↑(maname-deq() x y))
⊢ Dec(x = y ∈ MaName)

---

Latex:


\mforall{}x,y:MaName.    Dec(x  =  y)


By

(((InstLemma  `deq\_property`  [\mkleeneopen{}MaName\mkleeneclose{};  \mkleeneopen{}maname-deq()\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  )

---

Home Index