Added some lemmas

Added some lemmas on the interaction between ap and term formers, as well as a nondependent version of transport_forall.