proposition: Lemma prop_check_not: forall bs br, length bs = length br -> check_not bs br = true -> map (Lit.interp rho) br = map (fun l => negb (Lit.interp rho l)) bs.
proof: Proof. intro bs; induction bs; intros br Hlen Hcheck. - simpl in Hlen. symmetry in Hlen. apply empty_list_length in Hlen. rewrite Hlen; now simpl. - case br in *. + simpl in Hcheck; now contradict Hcheck. + simpl in Hlen. inversion Hlen as [Hlen']. simpl in Hcheck. rewrite andb_true_iff in Hcheck; destruct Hcheck as (Hcheck1, Hcheck2). apply Int63.eqb_spec in Hcheck1; rewrite Hcheck1. simpl. rewrite Lit.interp_neg. apply f_equal. apply IHbs; auto. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance