proposition: Lemma zextend_interp_all: forall a i, RAWBITVECTOR_LIST.zextend (map (Lit.interp rho) a) i = map (Lit.interp rho) (zextend_lit a i).
proof: Proof. intro a. induction a as [ | xa xsa IHa]. - intros. simpl. induction i. + intros. now simpl. + intros. unfold RAWBITVECTOR_LIST.zextend in *. simpl. rewrite IHi. assert (Lit.interp rho Lit._false = false). { specialize (Lit.interp_false rho wf_rho). intros. rewrite <- not_true_iff_false. unfold not in *. intros. now apply H. } now rewrite H. - intros. induction i. + now simpl. + unfold RAWBITVECTOR_LIST.zextend, zextend_lit in *. simpl in *. rewrite <- IHi. assert (Lit.interp rho Lit._false = false). { specialize (Lit.interp_false rho wf_rho). intros. rewrite <- not_true_iff_false. unfold not in *. intros. now apply H. } now rewrite H. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance