# 快瘋了

```pop-eq : ∀ {n m a} → {xs : Queue a (suc n)}{ys : Queue a (suc m)} → xs ∼ ys → (pop' xs) ∼ (pop' ys) pop-eq {n} {m} {a} {xs} {ys} qeq with front xs | rear xs | front ys | rear ys | length-sum xs | length-sum ys | length-eq qeq | pop' xs | pop' ys pop-eq qeq | .0 , [] | .0 , [] | n' , fs' | m0 , rs' | () | pf | refl | xs' | ys' pop-eq qeq | .0 , [] | suc n , (f ∷ fs) | .0 , [] | .0 , [] | refl | () | refl | xs' | ys' pop-eq qeq | .0 , [] | suc n , (r ∷ rs) | .0 , [] | .(suc n) , (r' ∷ rs') | refl | refl | refl | xs' | ys' = {!  !} pop-eq qeq | .0 , [] | suc .(n' + m') , (r ∷ rs) | (suc n') , (f' ∷ fs') | m' , rs' | refl | refl | refl | xs' | ys' = {! !} pop-eq qeq | suc n , (f ∷ fs) | m , rs | .0 , [] | .(suc (n + m)) , rs' | refl | refl | refl | xs' | ys' = {!  !} pop-eq qeq | suc n , (f ∷ fs) | m , rs | (suc n') ,(f' ∷ fs') | m' , rs' | refl | pf2 | refl | xs' | ys' = {! !} `````` push-eq : ∀ {n m a} → {xs : Queue a n}{ys : Queue a m}{x : a} → xs ∼ ys → (push xs x) ∼ (push ys x) push-eq {n} {m} {a} {xs} {ys} {x} qeq with length-sum xs | length-sum ys | length-eq qeq push-eq {.(n + m)} {.(n' + m')} {a} {que {n} {m} fs rs} {que {n'} {m'} fs' rs'} {x} qeq | refl | refl | pf with push (que fs rs) x | push (que fs' rs') x ... | xs' | ys' with front xs' | rear xs' | front ys' | rear ys' ... | n1 , fs1 | m1 , rs1 | n2 , fs2 | m2 , rs2 = {! !}```