proposition: Lemma List_eq : forall (l m: list bool), beq_list l m = true <-> l = m.
proof: Proof. induction l; destruct m; simpl; split; intro; try (reflexivity || discriminate). - rewrite andb_true_iff in H. destruct H. rewrite eqb_true_iff in H. rewrite H. apply f_equal. apply IHl. exact H0. - inversion H. subst b. subst m. rewrite andb_true_iff. split. + apply eqb_reflx. + apply IHl; reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance