---

Step * of Lemma dec_iff_ex_bvfun

∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (∀x,y:T.  Dec(E[x;y]) ⇐⇒ ∃f:T ⟶ T ⟶ 𝔹. ∀x,y:T.  (↑(x f y) ⇐⇒ E[x;y]))
BY
{ ((Unfolds ``infix_ap so_apply`` 0 THENM GenRepD) THENA Auto) }

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

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}x,y:T.    Dec(E[x;y])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x,y:T.    (\muparrow{}(x  f  y)  \mLeftarrow{}{}\mRightarrow{}  E[x;y]))


By

---

Latex:
((Unfolds  ``infix\_ap  so\_apply``  0  THENM  GenRepD)  THENA  Auto)

---

Home Index