Step * 1 1 1 1 of Lemma decidable__quotient_equal

.....assertion..... 
1. [T] Type
2. [E] T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E[x;y])
4. T ⟶ T ⟶ 𝔹
5. ∀x,y:T.  (↑(x y) ⇐⇒ E[x;y])
⊢ f ∈ (x,y:T//E[x;y]) ⟶ (x,y:T//E[x;y]) ⟶ 𝔹
BY
(ExtWith [`u'] [⌜T ⟶ T ⟶ 𝔹⌝THENA Auto) }

1
1. Type
2. T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E[x;y])
4. T ⟶ T ⟶ 𝔹
5. ∀x,y:T.  (↑(x y) ⇐⇒ E[x;y])
6. x,y:T//E[x;y]
⊢ u ∈ (x,y:T//E[x;y]) ⟶ 𝔹


Latex:


Latex:
.....assertion..... 
1.  [T]  :  Type
2.  [E]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(T;x,y.E[x;y])
4.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
5.  \mforall{}x,y:T.    (\muparrow{}(x  f  y)  \mLeftarrow{}{}\mRightarrow{}  E[x;y])
\mvdash{}  f  \mmember{}  (x,y:T//E[x;y])  {}\mrightarrow{}  (x,y:T//E[x;y])  {}\mrightarrow{}  \mBbbB{}


By


Latex:
(ExtWith  [`u']  [\mkleeneopen{}T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}\mkleeneclose{}]  THENA  Auto)




Home Index