---

Step * 1 1 4 of Lemma gen_hyp_tp


1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
5. A ∈ Type
6. e ∈ A
7. ∀x:A. (e = x ∈ A ∈ Type)
⊢ {{False ⇒ True}}
BY
{ (\p.
 let i = get_int_arg `i` p
 in let x = get_term_arg `x` p
 in let e = get_term_arg `e` p
 in let A = get_term_arg `A` p
 in
   AssertAtHyp
    i
    (mk_exists_term (dv x) A (mk_equal_term A e x))
    p) }

1
.....assertion..... 
1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
5. A ∈ Type
6. e ∈ A
7. ∀x:A. (e = x ∈ A ∈ Type)
⊢ ∃x:A. (e = x ∈ A)

2
1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. ∃x:A. (e = x ∈ A)
5. z : H e
6. A ∈ Type
7. e ∈ A
8. ∀x:A. (e = x ∈ A ∈ Type)
⊢ {{False ⇒ True}}

---

Latex:

---

Latex:

1.  A  :  Type
2.  e  :  A
3.  H  :  A  {}\mrightarrow{}  \mBbbU{}\{j\}
4.  z  :  H  e
5.  A  \mmember{}  Type
6.  e  \mmember{}  A
7.  \mforall{}x:A.  (e  =  x  \mmember{}  Type)
\mvdash{}  \{\{False  {}\mRightarrow{}  True\}\}


By

---

Latex:
(\mbackslash{}p.
  let  i  =  get\_int\_arg  `i`  p
  in  let  x  =  get\_term\_arg  `x`  p
  in  let  e  =  get\_term\_arg  `e`  p
  in  let  A  =  get\_term\_arg  `A`  p
  in
      AssertAtHyp
        i
        (mk\_exists\_term  (dv  x)  A  (mk\_equal\_term  A  e  x))
        p)

---

Home Index