proposition: Lemma length_shr_lit_be: forall a, length (_shr_lit_be a) = length a.
proof: Proof. intro a. induction a; intros. - now simpl. - unfold _shr_lit_be. simpl. case_eq a0; intros. + easy. + simpl. apply f_equal. case_eq l; intros. now simpl. simpl. now rewrite helper2. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance