Function lam_id 

pub fn lam_id<A: Prop, B: Prop, X: Prop, N: Nat>(
    ty_x: Ty<X, Type<N>>,
    ty_b: Ty<B, X>,
) -> Eq<App<LamId<A, X>, B>, B>

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