proposition: Lemma List_eq_refl : forall (l: list bool), beq_list l l = true.
proof: Proof. induction l; simpl; try (reflexivity || discriminate). - rewrite andb_true_iff. split. apply eqb_reflx. apply IHl. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance