Function prop::fun::fun_ext_app_eq_from_eq

pub fn fun_ext_app_eq_from_eq<F: Prop, G: Prop, A: Prop, X: Prop>(
    ty_a: Ty<A, X>,
    eq: Eq<F, G>
) -> App<FunExtAppEq<F, G, A, X>, Tup3<F, G, A>>

(a : x) ⋀ (f == g) => ((\(a : x) = (f(a) == g(a))) . (snd . snd))((f, g, a)).