---

Step * 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 : {x:T| P[x]} 
6. y : {x:T| P[x]} 
⊢ uiff(↑(x eq y);x = y ∈ {x:T| P[x]} )
BY
{ D 5 THEN D 7 THEN InstHyp [x; y] 4 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 : 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]} )

---

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


By

---

Latex:
D  5  THEN  D  7  THEN  InstHyp  [x;  y]  4  THENW  Auto\mcdot{}

---

Home Index