Hooray!!

哈哈！硬是把 isort-der 擠出來了！XD 可是 code 非常暴力，節錄一個 subcase 給大家參觀一下：

... | no  a≰b = exists {_} {_} {b ∷ insert a x} (inj₂ (exists {_} {_} {b ,
insert a x} ((≡-refl , insert⊑combine (a , x) (insert a x) ≡-refl) ,
≡-refl)) , exists {_} {_} {b , insert a x} ((≡-refl , insert-respects-order
a x (≡-subst (ordered? x) (≡-sym (ordered?⊑idR x x' foldR-x-x'))
foldR-x-x')) , exists {_} {_} {b , insert a x} ((≡-refl , insert-respects-lbound
a b x (≡-subst₂ (\b x -> lbound (b , x)) (≡-sym b≡b') (≡-sym (ordered?⊑idR
x x' foldR-x-x')) lbound-b',x') (<-relax (≰-elim a≰b))) , insert-a-b∷x≡y)))

顯然還需要用力修整一番 XD。

--
改長輩寫的東西真是超恐怖…