Added two proofs to the Lists library. The first, Forall_inv_tail, extends Forall_inv to assert that a property that is true for every element of a list is true for every element in the tail of the list. The second, Exists_impl, parallels Forall_impl and proves that if there exists an element in a list that satisfies a given predicate, and the predicate implies another proposition, then there exists an element in the list that satisfies the implied proposition. Both of these proofs fill natural gaps within the List library.

0 files changed, 0 insertions, 0 deletions