proposition: Lemma list_inject : forall (A:Set)(a b :A)(l l':list A), a :: b :: l = b :: a :: l' -> a = b /\ l = l'.
proof: Proof. intros A a b l l' e. injection e. auto. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List