---

Step * 1 1 of Lemma dec_iff_ex_bvfun


1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. g : ∀x,y:T.  ((E x y) ∨ (¬(E x y)))@i
⊢ ∀x,y:T.  (↑case g x y of inl(a) => tt | inr(b) => ff ⇐⇒ E x y)
BY
{ (RepD THENA Auto) }

1
1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. g : ∀x,y:T.  ((E x y) ∨ (¬(E x y)))@i
4. x : T@i
5. y : T@i
⊢ ↑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  :  \mforall{}x,y:T.    ((E  x  y)  \mvee{}  (\mneg{}(E  x  y)))@i
\mvdash{}  \mforall{}x,y:T.    (\muparrow{}case  g  x  y  of  inl(a)  =>  tt  |  inr(b)  =>  ff  \mLeftarrow{}{}\mRightarrow{}  E  x  y)


By

---

Latex:
(RepD  THENA  Auto)

---

Home Index