proposition: Lemma length_nshl_lit_be: forall n a, length (nshl_lit_be a n) = length a.
proof: Proof. intros n. induction n; intros. - now simpl. - simpl. rewrite (IHn (_shl_lit_be a)). simpl. unfold nshl_lit_be. now rewrite length_shl_lit_be. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance