proposition: Lemma prop_check_bbc2: forall l bs, check_bbc l bs = true -> RAWBITVECTOR_LIST.beq_list l (map (Lit.interp rho) bs) = true.
proof: Proof. intro l. induction l as [ | xl xsl IHl ]. - intros. simpl in *. case bs in *. now simpl. now contradict H. - intros. simpl in H. case bs in *. now contradict H. simpl. case_eq (Lit.is_pos i); intros. rewrite H0 in H. case_eq (t_form .[ Lit.blit i]); intros; try (rewrite H1 in H; now contradict H). rewrite H1 in H. case xl in *. rewrite andb_true_iff. split. unfold Lit.interp. rewrite H0. unfold Var.interp. specialize (rho_interp (Lit.blit i)). rewrite H1 in rho_interp. simpl in rho_interp. rewrite rho_interp. easy. apply IHl; easy. now contradict H. rewrite H1 in H. case xl in *. now contradict H. rewrite andb_true_iff. split. specialize (rho_interp (Lit.blit i)). rewrite H1 in rho_interp. simpl in rho_interp. unfold Lit.interp. rewrite H0. unfold Var.interp. rewrite rho_interp. easy. apply IHl; easy. rewrite H0 in H. now contradict 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