proposition: Lemma length__shr_be: forall a, length (_shr_be a) = length a.
proof: Proof. intro a. induction a; intros. - now simpl. - simpl. rewrite <- IHa. case_eq a0; easy. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance