Step
*
of Lemma
eqfun_p_subtyping
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[eq:T ⟶ T ⟶ 𝔹]. IsEqFun({x:T| P[x]} ;eq) supposing IsEqFun(T;eq)
BY
{ ((UnivCD THENA Auto) THEN OnAllClauses (\i. Try (Unfolds ``eqfun_p`` i)) THENW Auto) }
1
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]} )
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}]. \mforall{}[eq:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbB{}]. IsEqFun(\{x:T| P[x]\} ;eq) supposing IsEqFun(T;eq)
By
Latex:
((UnivCD THENA Auto) THEN OnAllClauses (\mbackslash{}i. Try (Unfolds ``eqfun\_p`` i)) THENW Auto)
Home
Index