proposition: Lemma check_not_length: forall bs br, check_not bs br = true -> length bs = length br.
proof: Proof. intro bs; induction bs; intros br Hcheck. - case br in *. + auto. + simpl in Hcheck; now contradict Hcheck. - case br in *. + simpl in Hcheck; now contradict Hcheck. + simpl in *. rewrite andb_true_iff in Hcheck. destruct Hcheck as (_, Hcheck'). apply IHbs in Hcheck'; 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