fact: Parameter L2s_ok : forall f (x y : L f), x >L y <-> In (x,y) (L2s f).
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)