Step
*
of Lemma
p-lift_wf
∀[A,B:Type]. ∀[P:A ⟶ ℙ]. ∀[d:x:A ⟶ Dec(P[x])]. ∀[f:{x:A| P[x]}  ⟶ B].  (p-lift(d;f) ∈ A ⟶ (B + Top))
BY
{ (Unfold `p-lift` 0 THEN Auto THEN (Fold `or` 0 THEN Fold `decidable` 0⋅) THEN Auto) }
Latex:
Latex:
\mforall{}[A,B:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:x:A  {}\mrightarrow{}  Dec(P[x])].  \mforall{}[f:\{x:A|  P[x]\}    {}\mrightarrow{}  B].
    (p-lift(d;f)  \mmember{}  A  {}\mrightarrow{}  (B  +  Top))
By
Latex:
(Unfold  `p-lift`  0  THEN  Auto  THEN  (Fold  `or`  0  THEN  Fold  `decidable`  0\mcdot{})  THEN  Auto)
Home
Index