proposition: Lemma coqhammer_example l1 l2 x y1 y2 y3: implb (orb (inlist x l1) (orb (inlist x l2) (orb (x =? y1) (inlist x (y2 ::y3::nil))))) (inlist x (y1::(l1 ++ (y2 :: (l2 ++ (y3 :: nil)))))).
proof: Proof. Proof using dec_Zlist in_eq in_cons in_or_app in_nil in_inv inlist_app_comm_cons. verit_no_check. Qed.
imports: SMTCoq Bool PArray Int63 List ZArith