work on morecoq -- [apply] tactic. can the theorem be proved without apply? also commented out [admit.] in lists.v