proposition: Lemma lxor_neg : forall l1 l2, (l1 lxor l2 =? 1) = true -> l1 = Lit.neg l2.
proof: Proof. unfold Lit.neg; intros l1 l2;rewrite eqb_spec;intros Heq;rewrite <- Heq. rewrite lxorC, <- lxorA, lxor_nilpotent, lxor0_r;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring