proposition: Lemma Fs_lab_ok : forall f : Sig', In f Fs_lab.
proof: Proof. intros [f l]. unfold Fs_lab. rewrite in_flat_map. exists f. split. apply Fs_ok. rewrite in_map_iff. exists l. intuition. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)