proposition: Lemma not_list_length: forall a, length a = length (map negb a).
proof: Proof. intro a. induction a as [ | a xs IHxs]. - auto. - simpl. apply f_equal. exact IHxs. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance