made dummy arguments of F and G explicit (as an incentive to get rid of them)
previous commit must have broken proof of lemma ll42 (will fix later)