Skip to main content

lam

prop::fun

Function lam 

Source 
pub fn lam<A: Prop, B: Prop, X: Prop, C: Prop>(
    _ty_c: Ty<C, X>,
) -> Eq<App<Lam<Ty<A, X>, B>, C>, Subst<B, A, C>>
Expand description

(c : x) => ((\(a : x) = b)(c) == b[a := c]).