proposition: Lemma sub_restrict s t : sub s t = sub (restrict s (vars t)) t.
proof: Proof. apply sym_eq. apply sub_eq_vars_sub. apply sub_eq_restrict. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)