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