---

Step * of Lemma gen_hyp_tp

∀[A:Type]. ∀[e:A]. ∀[H:A ⟶ 𝕌{j}]. ∀[z:H e].  {{{False ⇒ True}}}
BY
{ (UnivCD THENA Auto) }

1
1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
⊢ {{False ⇒ True}}

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[e:A].  \mforall{}[H:A  {}\mrightarrow{}  \mBbbU{}\{j\}].  \mforall{}[z:H  e].    \{\{\{False  {}\mRightarrow{}  True\}\}\}


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index