proposition: Lemma trichotomy_restriction : forall x y l, In x l -> In y l -> trichotomy R x y -> trichotomy (restriction R l) x y.
proof: Proof. unfold trichotomy, restriction. intros. tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)