Function prop::fun::lam_app_trivial

source · 
pub fn lam_app_trivial<A: Prop, B: Prop, X: Prop>(
    ty_b: Ty<B, X>
) -> Eq<App<Lam<Ty<A, X>, B>, B>, B>
Expand description

(b : x) => ((\(a : x) = b)(b) == b.