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