Coq
Inductive nat_list : Set := NNil : nat_list NCons : nat -> nat_list -> nat_list. Fixpoint nlength (ls : nat_list) : nat := match ls with NNil => O NCons _ ls' => S (nlength ls') end.Fixpoint napp (ls1 ls2 : nat_list) : nat_list := match ls…
Inductive nat_list : Set := NNil : nat_list NCons : nat -> nat_list -> nat_list. Fixpoint nlength (ls : nat_list) : nat := match ls with NNil => O NCons _ ls' => S (nlength ls') end.Fixpoint napp (ls1 ls2 : nat_list) : nat_list := match ls…