proposition: Lemma mk_list_false_eq: forall bs, (map (fun _ : int => Lit.interp rho Lit._false) bs) = (RAWBITVECTOR_LIST.mk_list_false (Datatypes.length bs)).
proof: Proof. intro bs. induction bs as [ | xbs xsbs IHbs ]. - now simpl. - simpl. rewrite IHbs. specialize (@Lit.interp_false rho wf_rho). intros. unfold is_true in H. apply not_true_is_false in H. now rewrite H. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance