proposition: Lemma sub_eq_vars_sub s1 s2 t : sub_eq_dom s1 s2 (vars t) -> sub s1 t = sub s2 t.
proof: Proof. intro. eapply sub_eq_dom_incl_sub. apply H. refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)