proposition: Lemma dup_int_context_spec : forall c s l, dup_int_term (fill c (sub s l)) = fill (dup_int_context c) (sub (dup_int_subst s) (dup_int_term l)).
proof: Proof. induction c; intros. simpl. rewrite dup_int_subst_spec. apply eq_refl. simpl. cut (Vmap dup_int_term (Vcast (Vapp t (Vcons (fill c (sub s l)) t0)) e) = (Vcast (Vapp (Vmap dup_int_term t) (Vcons (fill (dup_int_context c) (sub (dup_int_subst s) (dup_int_term l))) (Vmap dup_int_term t0))) e)). intro. rewrite H; auto. rewrite Vmap_cast, Vmap_app. simpl. rewrite IHc. auto. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)