proposition: Lemma length_shl_be: forall a b, length a = length (shl_lit_be a b).
proof: Proof. intros. unfold shl_lit_be. now rewrite length_nshl_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