proposition: Lemma beqI_ok : rel_of_bool beqI << IR I (@eq I).
proof: Proof. intros t u. unfold rel_of_bool. destruct t; destruct u; simpl; intros; try discr. rewrite beq_nat_ok in H. subst. intro. refl. rewrite beq_symb_ok in H. subst. intro. refl. Qed.
imports: CoLoR(ATrs LogicUtil ListUtil VecUtil BoolUtil EqUtil ASemLab SN NatUtil RelUtil AWFMInterpretation)