proposition: Lemma length_shr_be: forall a b n, n = (length a) -> n = (length b)%nat -> n = (length (shr_be a b)).
proof: Proof. intros. unfold shr_be. now rewrite length_nshr_be. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance