Function prop::fun::fun_ext

source · 
pub fn fun_ext<F: Prop, G: Prop, X: Prop, Y: Prop, A: Prop>(
    tauto_eq_fg: Tauto<Eq<F, G>>
) -> FunExtTy<F, G, X, Y, A>
Expand description

(f == g)^true => fun_ext_ty(f, g).