(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/plist/props".
-
-include "plist/defs.ma".
+include "Base-1/plist/defs.ma".
theorem papp_ss:
\forall (is1: PList).(\forall (is2: PList).(eq PList (papp (Ss is1) (Ss