proposition: Lemma sextend_interp_zero: forall a, RAWBITVECTOR_LIST.sextend (map (Lit.interp rho) a) O = (map (Lit.interp rho) (sextend_lit a 0)).
proof: Proof. intros. unfold RAWBITVECTOR_LIST.sextend. case_eq a; intros; now simpl. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance