(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/RELATIONAL/NPlusList/props".
+
include "NPlusList/defs.ma".
(*
(*
intros. inversion H; clear H; intros;
[ id
- | subst.
+ | destruct.
*)
theorem npluslist_inj_2: \forall ns1,ns2,n.