---

Step * 1 of Lemma array-monad'_wf


1. Val : Type
2. n : ℕ
3. AType : array{i:l}(Val;n)
⊢ array-monad'(AType) ∈ Monad
BY
{ ((Unfold `array-monad\'` 0 THEN Auto) THEN Reduce 0 THEN Auto THEN Reduce 0 THEN Auto THEN Reduce (-1)) }

---

Latex:

---

Latex:

1.  Val  :  Type
2.  n  :  \mBbbN{}
3.  AType  :  array\{i:l\}(Val;n)
\mvdash{}  array-monad'(AType)  \mmember{}  Monad


By

---

Latex:
((Unfold  `array-monad\mbackslash{}'`  0  THEN  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto
  THEN  Reduce  (-1))

---

Home Index