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