proposition: Lemma undefined_hd_symb_dup_int_rules : forall f R, @defined Sig' (hd_symb Sig f) (dup_int_rules R) = false.
proof: Proof. induction R; intros. refl. simpl dup_int_rules. destruct a as [l r]. destruct l; hyp. Qed.
imports: Coq(Lia Compare_dec) CoLoR(ADecomp AUnif ARenCap ATrs ListUtil RelUtil AGraph LogicUtil AShift ACalls BoolUtil ADuplicateSymb ListDec EqUtil AHDE)