proposition: Lemma length_nshr_lit_be: forall n a, length (nshr_lit_be a n) = length a.
proof: Proof. intros n. induction n; intros. - now simpl. - simpl. rewrite (IHn (_shr_lit_be a)). simpl. unfold nshr_lit_be. now rewrite length_shr_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