pub type LamFst<A, X, B, Y> = Lam<Ty<A, X>, Lam<Ty<B, Y>, A>>;
\(a : x) = \(b : y) = a.
\(a : x) = \(b : y) = a