---

Step * 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)
⊢ ∀[x,y:{x:T| P[x]} ].  uiff(↑(x eq y);x = y ∈ {x:T| P[x]} )
BY
{ RepeatMFor 2 (D 0) THENW Auto }

1
1. T : Type
2. P : T ⟶ ℙ
3. eq : T ⟶ T ⟶ 𝔹
4. ∀[x,y:T].  uiff(↑(x eq y);x = y ∈ T)
5. x : {x:T| P[x]} 
6. y : {x:T| P[x]} 
⊢ uiff(↑(x eq y);x = y ∈ {x:T| P[x]} )

---

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)
\mvdash{}  \mforall{}[x,y:\{x:T|  P[x]\}  ].    uiff(\muparrow{}(x  eq  y);x  =  y)


By

---

Latex:
RepeatMFor  2  (D  0)  THENW  Auto

---

Home Index