---

Step * of Lemma bind-provision_wf

No Annotations
∀[T,S:𝕌']. ∀[x:Provisional(T)]. ∀[f:{t:T| allowed(x) ∧ (t = allow(x) ∈ T)}  ⟶ Provisional(S)].
  (bind-provision(x;t.f[t]) ∈ Provisional(S))
BY
{ (Intros THEN Unhide THEN Unfold `bind-provision` 0) }

1
1. T : 𝕌'
2. S : 𝕌'
3. x : Provisional(T)
4. f : {t:T| allowed(x) ∧ (t = allow(x) ∈ T)}  ⟶ Provisional(S)
⊢ provision(allowed(x) ∧ allowed(f[allow(x)]); allow(f[allow(x)])) ∈ Provisional(S)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T,S:\mBbbU{}'].  \mforall{}[x:Provisional(T)].  \mforall{}[f:\{t:T|  allowed(x)  \mwedge{}  (t  =  allow(x))\}    {}\mrightarrow{}  Provisional(S)].
    (bind-provision(x;t.f[t])  \mmember{}  Provisional(S))


By

---

Latex:
(Intros  THEN  Unhide  THEN  Unfold  `bind-provision`  0)

---

Home Index