proposition: Lemma prop_interp_firstn: forall xk' a, map (Lit.interp rho) (List.firstn xk' a) = (List.firstn xk' (map (Lit.interp rho) a)).
proof: Proof. intro xk'0. induction xk'0. + intros. now simpl. + intros. simpl. case a. now simpl. intros. simpl. apply f_equal. apply IHxk'0. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance