proposition: Lemma Fs_ok : forall f : Sig, In f Fs.
proof: Proof. intro. unfold Fs. rewrite (@In_fold_left _ _ _ (fun f => hd_symb S.Sig f :: int_symb S.Sig f :: nil)). simpl. right. destruct f; exists s; split_all; apply S.Fs_ok. refl. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)