---

Step * 1 of Lemma decidable__equal_MaName


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)
BY
{ (RW (AddrC [1] (HypC (-1))) 0 THEN Auto THEN DoSubsume THEN Auto) }

---

Latex:



1.  \mforall{}[x,y:MaName].    uiff(x  =  y;\muparrow{}(maname-deq()  x  y))
2.  x  :  MaName@i
3.  \mforall{}[y:MaName].  uiff(x  =  y;\muparrow{}(maname-deq()  x  y))
4.  y  :  MaName@i
5.  uiff(x  =  y;\muparrow{}(maname-deq()  x  y))
\mvdash{}  Dec(x  =  y)


By

(RW  (AddrC  [1]  (HypC  (-1)))  0  THEN  Auto  THEN  DoSubsume  THEN  Auto)

---

Home Index