Step
*
1
of Lemma
implies-usquash
1. T : ℙ
2. T
3. x : Top
⊢ x ∈ pertype(λx,y. T)
BY
{ ((PointwiseFunctionalityForEquality 3 THENW Auto) THEN PerEqCD_member⋅ THEN Reduce 0 THEN Auto) }
Latex:
Latex:
1. T : \mBbbP{}
2. T
3. x : Top
\mvdash{} x \mmember{} pertype(\mlambda{}x,y. T)
By
Latex:
((PointwiseFunctionalityForEquality 3 THENW Auto) THEN PerEqCD\_member\mcdot{} THEN Reduce 0 THEN Auto)
Home
Index