proposition: Lemma union_correct1 : sub_eq_dom union s1 l1.
proof: Proof. unfold sub_eq_dom, union. intros. case (eq_term_dec (s1 x) (Var x)); intros. case (In_dec eq_nat_dec x l2); intro. apply sym_eq. auto. ded (hyp2 _ n). rewrite e, H0. refl. refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)