List/build A0 (λ(list : Type) → λ(cons : A0 → list → list) → λ(nil : list) → x)