Preorder(ℤ;x,y.x | y){ (RepUnfolds ``preorder refl trans`` 0 THEN Auto) }1. ∀a:ℤ. (a | a)2. a : ℤ3. b : ℤ4. c : ℤ5. a | b6. b | c⊢ a | c