proposition: Lemma implies_lxor : tests -> lxor_test.
proof: Proof. move=> H. apply/forallInt8P=> x. apply idP. apply/forallInt8P=> y. apply idP. by move: (implies_binop H x y)=> /andP [_ /andP [_ /andP [_ /andP [-> _]]]]. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits) ExtrOcamlBasic