intros a b c ab bc
n : ℕ
⊢ ∀ (a b c : Variables n order.GrLex), Order.grlex a b → Order.grlex b c → Order.grlex a c
n : ℕ
a b c : Variables n order.GrLex
ab : Order.grlex a b
bc : Order.grlex b c
⊢ Order.grlex a c