Function app_map_eq 

pub fn app_map_eq<F: Prop, G: Prop, X: Prop>(
    _eq_fg: Eq<F, G>,
) -> Eq<App<F, X>, App<G, X>>

(f == g) => (f(x) == g(y)).

Lift equality of maps to application.