proposition: Lemma defined_list_ok : forall R f, defined f R = true <-> In f (list_defined R).
proof: Proof. induction R. simpl. intro; split; auto. intro H; discr. intro; destruct a as [l r]; simpl. destruct l. auto. rewrite In_cons, orb_eq, (IHR f), beq_symb_ok; tauto. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil VecUtil EqUtil BoolUtil) Coq(Sumbool)