-include "preamble.ma".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/insert_eq.con".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/unintro.con".
-
-inline procedural
-"cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/xinduction.con".