proposition: Lemma symb_ord_cons_var : forall R f g n r, symb_ord (mkRule (Var n) r :: R) f g -> symb_ord R f g.
proof: Proof. intros. destruct H as [x [H [H1 H2]]]. destruct (in_inv H). rewrite <-H0 in H1; simpl in H1; inversion H1. exists x; split; auto. Qed.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)