proposition: Lemma implies_unop : tests -> forall x, unop_tests x.
proof: Proof. move=> /andP [_ /andP [_ /andP[_ /andP [H _]]]] x. rewrite /succ_test. move: H=> /forallInt32P H. move: (H unop_tests)=> H'. apply H'=> x'. by apply idP. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits) ExtrOcamlBasic