proposition: Lemma List_eqP_refl : forall (l: list bool), beq_listP l l <-> l = l.
proof: Proof. intro l. induction l as [ | xl xsl IHl ]; intros. - easy. - simpl. repeat split. now apply IHl. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance