unfold Incomp
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ Incomp (Lexcomb r s) a b
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a