(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics".
-
-include "preamble.ma".
+include "Base-1/preamble.ma".
theorem insert_eq:
\forall (S: Set).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall (G: