proposition: Lemma beq_ok : forall f (l1 l2 : L f), beq l1 l2 = true <-> l1 = l2.
proof: Proof. intros f l1 l2. apply beq_vec_ok. apply @beq_symb_ok. Qed.
imports: CoLoR(ATrs LogicUtil ListUtil VecUtil BoolUtil EqUtil ASemLab SN NatUtil RelUtil AWFMInterpretation)