---

Step * of Lemma concat-unroll

∀a:Top. (concat(a) ~ if a is a pair then (fst(a)) @ concat(snd(a)) otherwise if a = Ax then [] otherwise ⊥)
BY
{ ((D 0 THENA Auto)
   THEN RepeatFor 2 (RW (AddrC [1] UnfoldTopAbC) 0)
   THEN RecUnfold `list_ind` 0
   THEN (Fold `reduce` 0 THEN Fold `concat` 0)
   THEN Reduce 0
   THEN SqReasoning) }

---

Latex:

---

Latex:
\mforall{}a:Top
    (concat(a)  \msim{}  if  a  is  a  pair  then  (fst(a))  @  concat(snd(a))
                              otherwise  if  a  =  Ax  then  []  otherwise  \mbot{})


By

---

Latex:
((D  0  THENA  Auto)
  THEN  RepeatFor  2  (RW  (AddrC  [1]  UnfoldTopAbC)  0)
  THEN  RecUnfold  `list\_ind`  0
  THEN  (Fold  `reduce`  0  THEN  Fold  `concat`  0)
  THEN  Reduce  0
  THEN  SqReasoning)

---

Home Index