---

Step * of Lemma fixpoint-induction-bottom-bar

∀[E,S:Type].  (∀[G:S ⟶ bar(E)]. ∀[g:S ⟶ S].  (G[fix(g)] ∈ bar(E))) supposing ((⊥ ∈ S) and mono(E) and value-type(E))
BY
{ (InstLemma `fixpoint-induction-bottom` [] THEN Unfold `bar` 0 THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[E,S:Type].
    (\mforall{}[G:S  {}\mrightarrow{}  bar(E)].  \mforall{}[g:S  {}\mrightarrow{}  S].    (G[fix(g)]  \mmember{}  bar(E)))  supposing 
          ((\mbot{}  \mmember{}  S)  and 
          mono(E)  and 
          value-type(E))


By

---

Latex:
(InstLemma  `fixpoint-induction-bottom`  []  THEN  Unfold  `bar`  0  THEN  Trivial)

---

Home Index