proposition: Lemma union_correct2 : sub_eq_dom union s2 l2.
proof: Proof. unfold sub_eq_dom, union. intros. case (eq_term_dec (s1 x) (Var x)); intros. refl. case (In_dec eq_nat_dec x l1); intro. auto. ded (hyp1 _ n0). contr. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)