---

Step * of Lemma is-list-approx_wf

∀T:Type. ∀j:ℕ.  (is-list-approx(j) ∈ colist(T) ⟶ partial(𝔹))
BY
{ (RepUR ``is-list-approx`` 0
   THEN InductionOnNat
   THEN Reduce 0
   THEN Auto
   THEN Try ((RWO "fun_exp_unroll_1" 0 THEN Auto THEN InstLemma `is-list-fun_wf` [⌜T⌝]⋅ THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}j:\mBbbN{}.    (is-list-approx(j)  \mmember{}  colist(T)  {}\mrightarrow{}  partial(\mBbbB{}))


By

---

Latex:
(RepUR  ``is-list-approx``  0
  THEN  InductionOnNat
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((RWO  "fun\_exp\_unroll\_1"  0  THEN  Auto  THEN  InstLemma  `is-list-fun\_wf`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THEN  Auto)))

---

Home Index