---

Step * of Lemma has-value-equality-fix-bar

∀[T,E,S:Type].  ∀[G:T ⟶ bar(E)]. ∀[g:T ⟶ T].  ((G fix(g))↓ ∈ ℙ) supposing value-type(E) ∧ (⊥ ∈ T)
BY
{ TACTIC:TACTIC:(UnivCD THENA (Try (Complete (Auto)) THEN MemCD THEN Try (BLemma `bottom-member-prop`) THEN Auto)) }

1
1. T : Type
2. E : Type
3. S : Type
4. value-type(E) ∧ (⊥ ∈ T)
5. G : T ⟶ bar(E)
6. g : T ⟶ T
⊢ (G fix(g))↓ ∈ ℙ

---

Latex:

---

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


By

---

Latex:
TACTIC:TACTIC:(UnivCD
                              THENA  (Try  (Complete  (Auto))
                                            THEN  MemCD
                                            THEN  Try  (BLemma  `bottom-member-prop`)
                                            THEN  Auto)
                              )

---

Home Index