proposition: Lemma sub_eq_dom_incl_sub s1 s2 l : sub_eq_dom s1 s2 l -> forall t, incl (vars t) l -> sub s1 t = sub s2 t.
proof: Proof. intros until t. unfold sub_eq_dom in H. apply term_ind with (P := fun t => incl (vars t) l -> sub s1 t = sub s2 t) (Q := fun n (ts : terms n) => incl (vars_vec ts) l -> Vmap (sub s1) ts = Vmap (sub s2) ts). unfold incl. simpl. intuition. intros. rewrite !sub_fun. f_equal. apply H0. rewrite vars_fun in H1. hyp. refl. intros. rewrite vars_vec_cons in H2. unfold incl in H2. ded (incl_app_elim H2). destruct H3. simpl. apply Vcons_eq_intro; auto. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)