Check...

好啦，in-flatcat 終於 check 了，可是看看我證了一個什麼樣的 lemma…

in-flatcat : {A : Set} {n m : Nat} -> Braun A m -> List A ⋮ hasLength n ->
                                      List A ⋮ hasLength (m + n)
in-flatcat nul accum = accum
in-flatcat {A} (bin a p left right) accum with in-flatcat right accum
... | sub ys yslenpf = subst
                       (\x -> List A ⋮ hasLength x)
                       lemma
                       (in-flatcat left (sub (a :: ys) (len-step yslenpf)))
  where
    lemma : {n₁ n₂ n₃ : Nat} ->
            suc (parity p + (n₁ + n₂) + n₃) ≡ parity p + n₁ + suc (n₂ + n₃)
    lemma {n₁} {n₂} {n₃} =
      trans
        (trans
           (sym (cong suc (+assoc (parity p) (n₁ + n₂) n₃)))
           (trans
              (sym (+suc (parity p) (n₁ + n₂ + n₃)))
              (cong (\x -> parity p + x)
                    (trans
                       (cong suc (sym (+assoc n₁ n₂ n₃)))
                       (sym (+suc n₁ (n₂ + n₃)))))))
        (+assoc (parity p) n₁ (suc (n₂ + n₃)))

不是這樣搞的吧 XD。

--
似乎該來研究一下 Logic.ChainReasoning 了？XD