proposition: Lemma and_with_bool_len: forall a b, length (and_with_bool a (nth 0 b false)) = length a.
proof: Proof. intro a. - induction a. intros. now simpl. intros. simpl. now rewrite IHa. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance