---

Step * of Lemma n-tuple-decomp

∀[n:ℕ]. (n-tuple(n) ~ if (n =z 0) then Unit if (n =z 1) then Top else Top × n-tuple(n - 1) fi )
BY
{ ((RepUR ``n-tuple tuple-type`` 0 THEN InductionOnNat)
   THEN (OReduce 0 THENA Auto)
   THEN Try (Trivial)
   THEN (RW (AddrC [1;1;2] (LemmaC `upto_decomp2`)) 0 THENA Auto')
   THEN Reduce 0
   THEN (RWW "null-map null-upto" 0 THENA Auto)
   THEN AutoSplit
   THEN EqCD
   THEN Try (Trivial)
   THEN (RWO "map-map" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (n-tuple(n)  \msim{}  if  (n  =\msubz{}  0)  then  Unit  if  (n  =\msubz{}  1)  then  Top  else  Top  \mtimes{}  n-tuple(n  -  1)  fi  )


By

---

Latex:
((RepUR  ``n-tuple  tuple-type``  0  THEN  InductionOnNat)
  THEN  (OReduce  0  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  (RW  (AddrC  [1;1;2]  (LemmaC  `upto\_decomp2`))  0  THENA  Auto')
  THEN  Reduce  0
  THEN  (RWW  "null-map  null-upto"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  (RWO  "map-map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  Auto)

---

Home Index