---

Step * 1 of Lemma gen_hyp_tp


1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
⊢ {{False ⇒ True}}
BY
{ PushArgs
 [`x`,term_to_arg ⌜x⌝
 ;`e`,term_to_arg ⌜e⌝
 ;`A`,term_to_arg ⌜A⌝
 ;`UH`,term_to_arg ⌜𝕌{j}⌝
 ;`UA`,term_to_arg ⌜Type⌝
 ;`i`,int_to_arg 4] }

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

---

Latex:

---

Latex:

1.  A  :  Type
2.  e  :  A
3.  H  :  A  {}\mrightarrow{}  \mBbbU{}\{j\}
4.  z  :  H  e
\mvdash{}  \{\{False  {}\mRightarrow{}  True\}\}


By

---

Latex:
PushArgs
  [`x`,term\_to\_arg  \mkleeneopen{}x\mkleeneclose{}
  ;`e`,term\_to\_arg  \mkleeneopen{}e\mkleeneclose{}
  ;`A`,term\_to\_arg  \mkleeneopen{}A\mkleeneclose{}
  ;`UH`,term\_to\_arg  \mkleeneopen{}\mBbbU{}\{j\}\mkleeneclose{}
  ;`UA`,term\_to\_arg  \mkleeneopen{}Type\mkleeneclose{}
  ;`i`,int\_to\_arg  4]

---

Home Index