proposition: Lemma length_nshr_be: forall n a, length (nshr_be a n) = length a.
proof: Proof. intro n. induction n; intros; simpl. - reflexivity. - now rewrite (IHn (_shr_be a)), length__shr_be. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance