---

Step * 1 1 of Lemma gen_hyp_tp


1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
⊢ {{False ⇒ True}}
BY
{ (%S%
\p.
  let UA = get_term_arg `UA` p
  in let A = get_term_arg `A` p
  in let e = get_term_arg `e` p
  in let x = get_term_arg `x` p
  in
   AssertL
     [mk_member_term UA A
     ;mk_member_term A e
     ;mk_all_term (dv x) A (mk_member_term
                               UA (mk_equal_term A e x))
     ]
   p) }

1
.....assertion..... 
1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
⊢ A ∈ Type

2
.....assertion..... 
1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
5. A ∈ Type
⊢ e ∈ A

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

4
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}}

---

Latex:

---

Latex:

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


By

---

Latex:
(\%S\%
\mbackslash{}p.
    let  UA  =  get\_term\_arg  `UA`  p
    in  let  A  =  get\_term\_arg  `A`  p
    in  let  e  =  get\_term\_arg  `e`  p
    in  let  x  =  get\_term\_arg  `x`  p
    in
      AssertL
          [mk\_member\_term  UA  A
          ;mk\_member\_term  A  e
          ;mk\_all\_term  (dv  x)  A  (mk\_member\_term
                                                              UA  (mk\_equal\_term  A  e  x))
          ]
      p)

---

Home Index