---

Step * 1 1 1 1 1 of Lemma dec_iff_ex_bvfun


1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. g : x:T ⟶ (∀y:T. ((E x y) ∨ (¬(E x y))))
4. x : T@i
5. y : T@i
6. y1 : y:T ⟶ ((E x y) ∨ (¬(E x y)))
7. y1 = (g x) ∈ (∀y:T. ((E x y) ∨ (¬(E x y))))
8. y2 : (E x y) ∨ (¬(E x y))@i
9. y2 = (y1 y) ∈ ((E x y) ∨ (¬(E x y)))
⊢ ↑case g x y of inl(a) => tt | inr(b) => ff ⇐⇒ E x y
BY
{ D 8 }

1
1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. g : x:T ⟶ (∀y:T. ((E x y) ∨ (¬(E x y))))
4. x : T@i
5. y : T@i
6. y1 : y:T ⟶ ((E x y) ∨ (¬(E x y)))
7. y1 = (g x) ∈ (∀y:T. ((E x y) ∨ (¬(E x y))))
8. x1 : E x y@i
9. (inl x1) = (y1 y) ∈ ((E x y) ∨ (¬(E x y)))
⊢ ↑case g x y of inl(a) => tt | inr(b) => ff ⇐⇒ E x y

2
1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. g : x:T ⟶ (∀y:T. ((E x y) ∨ (¬(E x y))))
4. x : T@i
5. y : T@i
6. y1 : y:T ⟶ ((E x y) ∨ (¬(E x y)))
7. y1 = (g x) ∈ (∀y:T. ((E x y) ∨ (¬(E x y))))
8. y3 : ¬(E x y)@i
9. (inr y3 ) = (y1 y) ∈ ((E x y) ∨ (¬(E x y)))
⊢ ↑case g x y of inl(a) => tt | inr(b) => ff ⇐⇒ E x y

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [E]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  g  :  x:T  {}\mrightarrow{}  (\mforall{}y:T.  ((E  x  y)  \mvee{}  (\mneg{}(E  x  y))))
4.  x  :  T@i
5.  y  :  T@i
6.  y1  :  y:T  {}\mrightarrow{}  ((E  x  y)  \mvee{}  (\mneg{}(E  x  y)))
7.  y1  =  (g  x)
8.  y2  :  (E  x  y)  \mvee{}  (\mneg{}(E  x  y))@i
9.  y2  =  (y1  y)
\mvdash{}  \muparrow{}case  g  x  y  of  inl(a)  =>  tt  |  inr(b)  =>  ff  \mLeftarrow{}{}\mRightarrow{}  E  x  y


By

---

Latex:
D  8

---

Home Index