proposition: Lemma beq_lab_symb_ok : forall fl1 fl2, beq_lab_symb fl1 fl2 = true <-> fl1 = fl2.
proof: Proof. intros [f1 l1] [f2 l2]. simpl. split; intro. rewrite andb_eq in H. destruct H. rewrite beq_symb_ok in H. subst. rewrite beq_ok in H0. subst. refl. Leqtac. rewrite andb_eq, (beq_refl (@beq_symb_ok Sig)), beq_ok. auto. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)