Step
*
of Lemma
respects-equality-set-trivial
∀[T:Type]. ∀[P:T ⟶ ℙ]. respects-equality(T;{x:T| P[x]} )
BY
{ (Auto THEN D 0 THEN Auto THEN ParallelOp -2) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}]. respects-equality(T;\{x:T| P[x]\} )
By
Latex:
(Auto THEN D 0 THEN Auto THEN ParallelOp -2)
Home
Index