proposition: Lemma eqb_spec : forall l l', eqb l l' = true <-> l = l'.
proof: Proof. Proof eqb_spec. Lemma neg_involutive : forall l, neg (neg l) = l. Proof. unfold neg;intros; rewrite <- lxorA;change (1 lxor 1) with 0;rewrite lxor0_r;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring