---

Step * of Lemma append-unroll

∀[as,bs:Top].  (as @ bs ~ if as is a pair then [fst(as) / ((snd(as)) @ bs)] otherwise if as = Ax then bs otherwise ⊥)
BY
{ (Auto THEN RW (AddrC [1] UnfoldTopAbC) 0 THEN RecUnfold `list_ind` 0 THEN Fold `append` 0 THEN SqReasoning) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RW  (AddrC  [1]  UnfoldTopAbC)  0
  THEN  RecUnfold  `list\_ind`  0
  THEN  Fold  `append`  0
  THEN  SqReasoning)

---

Home Index