---

Step * 1 of Lemma decidable__mon_eq


1. g : Mon@i'
2. IsEqFun(|g|;=b)
3. a : |g|@i
4. b : |g|@i
⊢ Dec(a = b ∈ |g|)
BY
{ (UnfoldTopAb 2 THEN RW (HigherC (RevHypC 2)) 0  THENM ProveDecidable THENA Auto ) }

---

Latex:

---

Latex:

1.  g  :  Mon@i'
2.  IsEqFun(|g|;=\msubb{})
3.  a  :  |g|@i
4.  b  :  |g|@i
\mvdash{}  Dec(a  =  b)


By

---

Latex:
(UnfoldTopAb  2  THEN  RW  (HigherC  (RevHypC  2))  0    THENM  ProveDecidable  THENA  Auto  )

---

Home Index