proposition: Lemma check_concat_map: forall bs1 bs2, map (Lit.interp rho) bs1 ++ map (Lit.interp rho) bs2 = map (Lit.interp rho) (bs1 ++ bs2).
proof: Proof. intro bs1. induction bs1. - intros. now simpl. - intros. simpl. now rewrite IHbs1. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance