proposition: Lemma extract_interp_zero: forall a n, RAWBITVECTOR_LIST.extract (map (Lit.interp rho) a) 0 n = map (Lit.interp rho) (extract_lit a 0 n).
proof: Proof. intro a. induction a as [ | xa xsa IHa]. - intros. now simpl. - intros. simpl. case_eq n. now simpl. intros. simpl. apply f_equal. now rewrite IHa. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance