proposition: Lemma concat_len: forall (bs1 bs2 bsres: list bool), bs1 ++ bs2 = bsres -> ((length bs1) + (length bs2))%nat = (length bsres)%nat.
proof: Proof. intro bs1. induction bs1. - intros. simpl. simpl in H. now rewrite H. - intros. simpl. simpl in H. rewrite <- H. simpl. now rewrite app_length. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance