Function len_cons 

pub fn len_cons<X: Prop, A: Prop, B: Prop>(
    _: Ty<Cons<X, A, B>, List<A>>,
) -> Eq<Len<X, Cons<X, A, B>>, Succ<Len<X, B>>>

cons{x}(a, b) : list(a) => len{x}(cons{x}(a, b)) == succ(len{x}(b)).