proposition: Lemma prop_shl_be: forall a, RAWBITVECTOR_LIST._shl_be (map (Lit.interp rho) a) = (map (Lit.interp rho) (_shl_lit_be a)).
proof: Proof. intro a. case_eq a; intros. - now simpl. - unfold RAWBITVECTOR_LIST._shl_be, _shl_lit_be. simpl. 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 H0. } rewrite H0. apply f_equal. now rewrite map_lst. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance