proposition: Lemma lhs_fun_defined : forall (f : Sig) us r R, In (mkRule (Fun f us) r) R -> defined f R = true.
proof: Proof. induction R. auto. simpl. intro H. destruct H. subst a. simpl. rewrite (beq_refl (@beq_symb_ok Sig)). auto. destruct a. simpl. destruct lhs. auto. apply orb_intror. auto. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil VecUtil EqUtil BoolUtil) Coq(Sumbool)