---

Step * of Lemma do-apply-p-lift

∀[A,B:Type]. ∀[P:A ⟶ ℙ]. ∀[d:x:A ⟶ Dec(P[x])]. ∀[f:{x:A| P[x]}  ⟶ B]. ∀[x:A].
  do-apply(p-lift(d;f);x) = (f x) ∈ B supposing ↑can-apply(p-lift(d;f);x)
BY
{ ((Auto THEN MoveToConcl (-1)) THEN RepUR ``can-apply do-apply p-lift`` 0) }

1
1. A : Type
2. B : Type
3. P : A ⟶ ℙ
4. d : x:A ⟶ Dec(P[x])
5. f : {x:A| P[x]}  ⟶ B
6. x : A
⊢ (↑isl(case d x of inl(a) => inl (f x) | inr(a) => inr a ))
⇒ (outl(case d x of inl(a) => inl (f x) | inr(a) => inr a ) = (f x) ∈ B)

---

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].  \mforall{}[x:A].
    do-apply(p-lift(d;f);x)  =  (f  x)  supposing  \muparrow{}can-apply(p-lift(d;f);x)


By

---

Latex:
((Auto  THEN  MoveToConcl  (-1))  THEN  RepUR  ``can-apply  do-apply  p-lift``  0)

---

Home Index