Require drop_props.
Require pc3_props.
Require ty0_defs.
+Require ty0_gen.
Require ty0_lift.
Section ty0_correct. (****************************************************)
Hints Resolve ty0_shift : ltlc.
-(*#* #start file *)
-
Section ty0_unique. (*****************************************************)
+ Opaque pc3.
+
+(*#* #start file *)
+
(*#* #caption "uniqueness of types" *)
(*#* #cap #cap c, t1, t2 #alpha u in T *)