proposition: Lemma map_cons T U (f: T -> U) (h: T) (l: list T): map f (h :: l) = f h :: map f l.
proof: Proof. 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