---

Step * of Lemma polymorphic-list

∀f:⋂A:Type. (A ⟶ (A List)). ∃n:ℕ. (f = (λx.repn(n;x)) ∈ (⋂A:Type. (A ⟶ (A List))))
BY
{ (Auto THEN (InstLemma `polymorphic-constant-nat` [⌜λx.||f x||⌝]⋅ THENA Auto) THEN Reduce -1 THEN ParallelLast) }

1
1. f : ⋂A:Type. (A ⟶ (A List))
2. n : ℕ
3. ∀A:Type. ∀x:A.  (||f x|| = n ∈ ℕ)
⊢ f = (λx.repn(n;x)) ∈ (⋂A:Type. (A ⟶ (A List)))

---

Latex:

---

Latex:
\mforall{}f:\mcap{}A:Type.  (A  {}\mrightarrow{}  (A  List)).  \mexists{}n:\mBbbN{}.  (f  =  (\mlambda{}x.repn(n;x)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `polymorphic-constant-nat`  [\mkleeneopen{}\mlambda{}x.||f  x||\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  ParallelLast)

---

Home Index