include "coa_defs.ma".
-coercion Type_of_COA. (* this should be generated by the following line *)
-coercion coa. (* this should be inside coa_defs.moo but it isn't *)
+inductive True:Prop \def T:True.
-theorem zero_le: \forall (P:COA). \forall (p:P). le ? (zero P) p.
+theorem zero_le:
+ \forall (P:COA). \forall (p:P). (le ? (zero P) p) \to True.
+ intros.
+ exact T.
+qed.