---

Step * of Lemma det-id

∀[r:CRng]. ∀[n:ℕ].  (|I| = 1 ∈ |r|)
BY
{ (Auto
   THEN (InstLemma `deq-exists` [⌜ℕn ⟶ ℕn⌝]⋅ THENA Auto)
   THEN (Assert ∀x,y:ℕn ⟶ ℕn.  Dec(x = y ∈ (ℕn ⟶ ℕn)) BY
               (All Thin THEN Auto))
   THEN ThinTrivial
   THEN Thin 3
   THEN RenameVar `eq' (-1)) }

1
1. r : CRng
2. n : ℕ
3. eq : EqDecider(ℕn ⟶ ℕn)
⊢ |I| = 1 ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].    (|I|  =  1)


By

---

Latex:
(Auto
  THEN  (InstLemma  `deq-exists`  [\mkleeneopen{}\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mforall{}x,y:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n.    Dec(x  =  y)  BY
                          (All  Thin  THEN  Auto))
  THEN  ThinTrivial
  THEN  Thin  3
  THEN  RenameVar  `eq'  (-1))

---

Home Index