prov snoc_with_append, work through product types (a pair is a value of a product type, and forcing type inference makes things a bit confusing), skim MoreCoq.v -- tactics!