fact: Definition linear_extension R l R' := is_restricted R' l /\ (restriction R l) << R' /\ transitive R' /\ irreflexive R' /\ total R' l.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)