restored proof by turning F and G back into definitions: fun doesn't work here (possibly because we are talking about an infinite number of lists)