proposition: Lemma valid_check_bbVar lres : C.valid rho (check_bbVar lres).
proof: Proof. unfold check_bbVar. case_eq (Lit.is_pos lres); intro Heq1; [ |now apply C.interp_true]. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bs Heq0. case_eq (check_bb a bs 0 (Datatypes.length bs)); intro Heq2; [ |now apply C.interp_true]. unfold C.valid. simpl. rewrite orb_false_r. unfold Lit.interp. rewrite Heq1. unfold Var.interp. rewrite wf_interp_form; trivial. rewrite Heq0. simpl. apply bitOf_of_bits. intros. cut (Lit.interp rho 1 = false). intro Hr. rewrite <- Hr. rewrite map_nth. remember (@prop_checkbb' a bs Heq2 i). rewrite map_length in H. rewrite map_length. clear Heqe. now apply e in H. now apply rho_1. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance