---

Step * of Lemma provisional-monad_wf

No Annotations
provisional-monad{i:l}() ∈ Monad'
BY
{ (Unfold `provisional-monad` 0
   THEN MemCD
   THEN Reduce 0
   THEN Auto
   THEN Symmetry
   THEN BLemma `provisional-type-equality`
   THEN Auto
   THEN All (RepUR ``allowed allow bind-provision provision``)
   THEN All (Folds ``provision allowed allow``)
   THEN Auto
   THEN RepeatFor 2 ((∀h:hyp. ((FLemma `usquash-elim` [h] THENA Auto) THEN Thin h)  THEN ExRepD))
   THEN Auto
   THEN RepeatFor 2 (((BLemma `squash-implies-usquash` THEN Auto) THEN D 0 THEN Auto))) }

---

Latex:

---

Latex:
No  Annotations
provisional-monad\{i:l\}()  \mmember{}  Monad'


By

---

Latex:
(Unfold  `provisional-monad`  0
  THEN  MemCD
  THEN  Reduce  0
  THEN  Auto
  THEN  Symmetry
  THEN  BLemma  `provisional-type-equality`
  THEN  Auto
  THEN  All  (RepUR  ``allowed  allow  bind-provision  provision``)
  THEN  All  (Folds  ``provision  allowed  allow``)
  THEN  Auto
  THEN  RepeatFor  2  ((\mforall{}h:hyp.  ((FLemma  `usquash-elim`  [h]  THENA  Auto)  THEN  Thin  h)    THEN  ExRepD))
  THEN  Auto
  THEN  RepeatFor  2  (((BLemma  `squash-implies-usquash`  THEN  Auto)  THEN  D  0  THEN  Auto)))

---

Home Index