Type Alias AddRealTy 

pub type AddRealTy<X, A, Y> = DepTupTy<A, Real, AddRealLam<X, A, Y>>;

(a : real, (\(a : real) = (x == (a + y)))(a)).

Aliased Type

pub struct AddRealTy<X, A, Y>(/* private fields */);