proposition: Lemma root_lhsP : forall R f, In f (root_lhs_rules R) <-> exists a, In a R /\ root_eq f (lhs a) = true.
proof: Proof. induction R; simpl. intro. split; try tauto. intro. destruct H as [a [H _]]; auto. intro. destruct a as [[n| F vs] r]; simpl. split; intro. destruct (proj1 (IHR f) H) as [a [H0 H1]]. exists a; split; auto. destruct H as [a [H0 H1]]. destruct H0. destruct a as [[n' | F vs] r']. simpl in H1. inversion H1. inversion H. apply (IHR f). exists a; auto. split; intro. destruct H. exists (mkRule (Fun F vs) r). split. left; auto. simpl. rewrite H, beq_symb_ok; auto. destruct (proj1 (IHR f) H) as [a [H0 H1]]. exists a; split; auto. destruct H as [a [H H0]]. destruct H. destruct a as [[n | F' vs'] r']. inversion H0. inversion H. simpl in H0. rewrite <- H2, beq_symb_ok in H0; auto. right. apply (IHR f). exists a; auto. Qed.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)