proposition: Lemma defined_equiv : forall f R, defined f R = true <-> exists v, exists r, In (mkRule (Fun f v) r) R.
proof: Proof. intros. split. 2:{ intro. destruct H as [v [r H]]. apply (lhs_fun_defined f v r). auto. } intros. induction R. simpl in H. discr. simpl. simpl in H. destruct a as [a1 a2]. simpl in H. destruct a1. destruct (IHR H) as [v H0]; destruct H0 as [r H0]. exists v; exists r; auto. destruct (orb_prop _ _ H). 2:{ destruct (IHR H0) as [v' H1]. destruct H1 as [r H1]. exists v'; exists r. auto. } rewrite beq_symb_ok in H0; rewrite <- H0. exists t; exists a2. left; refl. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil VecUtil EqUtil BoolUtil) Coq(Sumbool)