Reverse.hss

flatten-module
consider 'rev
ww-split-param 1 [|wrap|] [|unwrap|]
bash
{consider lam ; alpha-lam 't}
any-call (unfold 'wrap)
any-call (unfold 'unwrap)
simplify
{rhs-of 'work
   alpha-lam 'ys
   lam-body
   eta-expand 'acc
   innermost case-float
   one-td (unfold-rule "repH ++")
   one-td (foreward (ww-fusion [| absH t |] [| repH t |] [| work xs |]))
   any-call (unfold-rule "repH (:)")
   simplify
   any-call (unfold-rule "repH []")
   any-call (unfold 'id)
}
any-call (unfold 'absH)