proposition: Theorem spec_lxor x y : [lxor x y] = Z.lxor [x] [y].
proof: Proof. rewrite lxor_fold. apply spec_same_level; clear x y. intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_lxor. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen