Import nat.
Import list.

def NS O =  \x /\X ((X N0 -> O) -> /\y ((X y -> O) ->  (X (S y) -> O)) -> (X x -> O)).

goal /\O,x (NS O x -> (N x -> O) -> O).
intro 3.
elim H.
trivial =.
trivial =.
save NStor.

print List.

def LS O =  \D,x /\X ((X nil -> O) -> /\a:D  /\y ((X y -> O) -> (X (a :: y) -> O)) -> (X x -> O)).


goal /\O,l (LS O (NS O) l -> (List N l -> O) -> O).
intro 3.
elim H.
auto =.
intros.
apply NStor with a then H0.
auto.
save LNStor.