(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/types/props".
-
-include "types/defs.ma".
+include "Base-1/types/defs.ma".
theorem ex2_sym:
\forall (A: Set).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to