proposition: Lemma concat_map : forall (A B : Set) (f : A -> B) (l0 l1 : list A), map f (l0 ++ l1) = (map f l0) ++ (map f l1).
proof: Proof. induction l0 as [ | xl0 xsl0 IHl0]; intros. - now simpl. - simpl. now rewrite IHl0. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance