un-inline different-drop
authorHelmut Grohne <helmut@subdivi.de>
Fri, 14 Dec 2012 11:03:04 +0000 (12:03 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Fri, 14 Dec 2012 11:03:04 +0000 (12:03 +0100)
Precond.agda

index 44512b3..76875a7 100644 (file)
@@ -56,7 +56,7 @@ different-∉ x (y ∷ ys) p (there pxs) = different-∉ x ys (different-drop y
 
 different-assoc : {m n : ℕ} → (u : Vec (Fin n) m) → (v : Vec Carrier m) → all-different u → ∃ λ h → assoc u v ≡ just h
 different-assoc []       []       p = empty , refl
-different-assoc (u ∷ us) (v ∷ vs) p with different-assoc us vs (λ i j i≢j → p (suc i) (suc j) (i≢j ∘ suc-injective))
+different-assoc (u ∷ us) (v ∷ vs) p with different-assoc us vs (different-drop u us p)
 different-assoc (u ∷ us) (v ∷ vs) p | h , p' = insert u v h , (begin
   assoc (u ∷ us) (v ∷ vs)
     ≡⟨ refl ⟩