---

Step * of Lemma assert-finite-fun-deq

No Annotations
∀[T:Type]. ∀[k:ℕ]. ∀[eq:EqDecider(T)]. ∀[f,g:ℕk ⟶ T].  uiff(↑(finite-fun-deq(k;eq) f g);f = g ∈ (ℕk ⟶ T))
BY
{ ((UnivCD THENA Auto) THEN RWO "assert-deq" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[k:\mBbbN{}].  \mforall{}[eq:EqDecider(T)].  \mforall{}[f,g:\mBbbN{}k  {}\mrightarrow{}  T].    uiff(\muparrow{}(finite-fun-deq(k;eq)  f  g);f  =  g)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "assert-deq"  0  THEN  Auto)

---

Home Index