proposition: Lemma check_bbc_length : forall bv bs, check_bbc bv bs = true -> length bv = length bs.
proof: Proof. intro bv. induction bv. intro bs. case bs. simpl; trivial. simpl; easy. intro bs. case bs in *. simpl; easy. simpl. case (Lit.is_pos i); try easy. case (t_form .[ Lit.blit i]); try easy; case a; try easy; intro Hc; apply IHbv in Hc; now rewrite Hc. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance