proposition: Lemma sub_union2 t : incl (vars t) l2 -> sub union t = sub s2 t.
proof: Proof. intro. eapply sub_eq_dom_incl_sub. apply union_correct2. hyp. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)