---

Step * 1 1 1 of Lemma eqfun_p_subtyping


1. T : Type
2. P : T ⟶ ℙ
3. eq : T ⟶ T ⟶ 𝔹
4. ∀[x,y:T].  uiff(↑(x eq y);x = y ∈ T)
5. x : T
6. [%2] : P[x]
7. y : T
8. [%4] : P[y]
9. uiff(↑(x eq y);x = y ∈ T)
⊢ uiff(↑(x eq y);x = y ∈ {x:T| P[x]} )
BY
{ RWHH 9 0 THEN Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbP{}
3.  eq  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
4.  \mforall{}[x,y:T].    uiff(\muparrow{}(x  eq  y);x  =  y)
5.  x  :  T
6.  [\%2]  :  P[x]
7.  y  :  T
8.  [\%4]  :  P[y]
9.  uiff(\muparrow{}(x  eq  y);x  =  y)
\mvdash{}  uiff(\muparrow{}(x  eq  y);x  =  y)


By

---

Latex:
RWHH  9  0  THEN  Auto

---

Home Index