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 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.