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