---

Step * 2 1 of Lemma dec_iff_ex_bvfun


1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. f : T ⟶ T ⟶ 𝔹
4. ∀x,y:T.  (↑(f x y) ⇐⇒ E x y)
5. x : T@i
6. y : T@i
⊢ Dec(E x y)
BY
{ (RWO "4<" 0 THENA Auto) }

1
1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. f : T ⟶ T ⟶ 𝔹
4. ∀x,y:T.  (↑(f x y) ⇐⇒ E x y)
5. x : T@i
6. y : T@i
⊢ Dec(↑(f x y))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [E]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
4.  \mforall{}x,y:T.    (\muparrow{}(f  x  y)  \mLeftarrow{}{}\mRightarrow{}  E  x  y)
5.  x  :  T@i
6.  y  :  T@i
\mvdash{}  Dec(E  x  y)


By

---

Latex:
(RWO  "4<"  0  THENA  Auto)

---

Home Index