gistfile1.txt

weave∙partition≡id : ∀ {A} {m n m+n : ℕ} {mn-proof : m + n ≅ m+n}
                                     fn (vec : Vec A (m + n)) →
                                   weave (partition {A} {m} {n} fn vec) ≅ vec
weave∙partition≡id {A} {0} fn [] = refl
weave∙partition≡id {A} {suc m} {0} fn (x ∷ xs) =
  cong (_∷_ x) (weave∙partition≡id {A} {m} {_} {_} {+0 m} fn xs)
weave∙partition≡id {A} {0} {suc n} fn (x ∷ xs) = 
  cong (_∷_ x) (weave∙partition≡id {A} {0} {_} {_} {refl} fn xs)
weave∙partition≡id {A} {suc m} {suc n} fn (x ∷ xs) with fn x
... | true = cong (_∷_ x) (weave∙partition≡id {A} {m} {_} {_} {refl} fn xs)
... | false =  begin
                subst (Vec A) (sym (cong suc (suc+ m n)))
                (x ∷ weave (partition {A} {suc m} fn (subst (Vec A) (suc+ m n) xs)))
              ≅⟨ {!!} ⟩
                x ∷ weave (partition {A} {suc m} {n} fn (smash xs))
              ≅⟨ cong (_∷_ x) (weave∙partition≡id {A} {suc m} {_} {_} {refl} fn 
                              (smash xs)) ⟩
                x ∷ (smash xs)
              ≅⟨ {!!} ⟩
                x ∷ xs
              ∎ 
            where smash : Vec A (m + suc n) → Vec A (suc (m + n))
                  smash = subst (Vec A) (suc+ m n)
                  smash-elim : Vec A (m + suc n) ≅ Vec A (suc (m + n))
                  smash-elim = cong (Vec A) (suc+ m n)