proposition: Lemma check_neg_length: forall bs bsres, check_neg bs bsres = true -> (length bs = length bsres)%nat.
proof: Proof. intros. unfold check_neg in H. specialize (@check_add_bvadd_length (map (fun l : int => Lit.neg l) bs) (map (fun _ : int => Lit._false) bs) bsres (Clit Lit._true)). intros. simpl in H0. specialize (H0 H). destruct H0. now rewrite map_length in H0. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance