:assume U  : *
:assume El : U -> *

:assume nat : U
:let Nat = El nat
:assume zero : Nat
:assume suc  : Nat -> Nat

:assume list : (a : U) -> U
:let List (A : U) = El (list A)
:assume nil  : (A : U) -> List A
:assume cons : (A : U) -> El A -> List A -> List A