QSort.hss

flatten-module
binding-of 'qsort
static-arg
{
    binding-of 'qsort'
    fix-intro
    def-rhs
    split-1-beta qsort [|absR|] [|repR|] ; assume
    rhs-of 'worker
    repeat (any-call (unfold ['.,'fix,'g,'repR,'absR]))
    simplify
    one-td (case-float-arg-lemma repHstrict) ; assume
    innermost let-float
    any-td (unfold-rule "repH ++") ; assume
    any-call (unfold-rule repH-absH-fusion) ; assume
    unshadow
    any-td (inline 'ds1)
    simplify
    alpha-let [worker]
    repeat (any-call (unfold-rules ["repH (:)","repH []"]))
    assume ; assume
}
repeat (any-call (unfold ['.,'absR, 'absH]))
innermost let-float
bash