Step * 1 1 of Lemma eqfun_p_subtyping


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

1
1. Type
2. T ⟶ ℙ
3. eq T ⟶ T ⟶ 𝔹
4. ∀[x,y:T].  uiff(↑(x eq y);x y ∈ T)
5. T
6. [%2] P[x]
7. 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