Function prop::fun::lam_lift

pub fn lam_lift<A: Prop, B: Prop, X: Prop>(
    ty_a: Ty<A, X>,
    b: B
) -> Lam<Ty<A, X>, B>

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