proposition: Lemma red_dup_int_hd_symb : forall f us v, red R' (Fun' (hd_symb f) us) v -> exists vs, v = Fun' (hd_symb f) vs.
proof: Proof. intros. redtac. destruct (in_map_elim lr). destruct H. destruct x. inversion H0. subst. destruct c; simpl in *. rewrite forallb_forall in hyp. ded (hyp _ lr). destruct lhs. discr. simpl dup_int_term in xl. simpl in xl. Funeqtac. discr. Funeqtac. exists (Vcast (Vapp t (Vcons (fill c (sub s (dup_int_term rhs))) t0)) e). refl. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)