proposition: Lemma sub_restrict_incl s (l r : term) : incl (vars r) (vars l) -> sub s r = sub (restrict s (vars l)) r.
proof: Proof. intro. rewrite sub_restrict. apply sub_eq_vars_sub. unfold sub_eq_dom. intros. unfold restrict. assert (Inb x (vars r) = true). apply Inb_intro. hyp. assert (Inb x (vars l) = true). apply Inb_intro. apply H. hyp. rewrite H1, H2. refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)