Function prop::fun::lam_id

pub fn lam_id<A: Prop, B: Prop, X: Prop>() -> Eq<App<LamId<A, X>, B>, B>

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