proposition: Lemma sub_union1 t : incl (vars t) l1 -> sub union t = sub s1 t.
proof: Proof. intro. eapply sub_eq_dom_incl_sub. apply union_correct1. hyp. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)