---

Step * 1 1 of Lemma bind-provision_wf

.....aux..... 
1. T : 𝕌'
2. S : 𝕌'
3. x : Provisional(T)
4. f : {t:T| allowed(x) ∧ (t = allow(x) ∈ T)}  ⟶ Provisional(S)
⊢ allowed(x) ∧ allowed(f[allow(x)]) ∈ Type
BY
{ (AndMemCD THENL [Auto; (RepeatFor 2 (MemCD) THEN Try (MemTypeCD) THEN Auto)]) }

---

Latex:

---

Latex:
.....aux..... 
1.  T  :  \mBbbU{}'
2.  S  :  \mBbbU{}'
3.  x  :  Provisional(T)
4.  f  :  \{t:T|  allowed(x)  \mwedge{}  (t  =  allow(x))\}    {}\mrightarrow{}  Provisional(S)
\mvdash{}  allowed(x)  \mwedge{}  allowed(f[allow(x)])  \mmember{}  Type


By

---

Latex:
(AndMemCD  THENL  [Auto;  (RepeatFor  2  (MemCD)  THEN  Try  (MemTypeCD)  THEN  Auto)])

---

Home Index