-definition reflexive1 ≝ λA:Type1.λR:A→A→CProp1.∀x:A.R x x.
-definition symmetric1 ≝ λC:Type1.λlt:C→C→CProp1. ∀x,y:C.lt x y → lt y x.
-definition transitive1 ≝ λA:Type1.λR:A→A→CProp1.∀x,y,z:A.R x y → R y z → R x z.
+definition reflexive1: ∀A:Type1.∀R:A→A→CProp1.CProp1 ≝ λA:Type1.λR:A→A→CProp1.∀x:A.R x x.
+definition symmetric1: ∀A:Type1.∀R:A→A→CProp1.CProp1 ≝ λC:Type1.λlt:C→C→CProp1. ∀x,y:C.lt x y → lt y x.
+definition transitive1: ∀A:Type1.∀R:A→A→CProp1.CProp1 ≝ λA:Type1.λR:A→A→CProp1.∀x,y,z:A.R x y → R y z → R x z.