proposition: Lemma sub_eq_dom_incl s1 s2 l1 l2 : sub_eq_dom s1 s2 l2 -> incl l1 l2 -> sub_eq_dom s1 s2 l1.
proof: Proof. unfold sub_eq_dom. auto. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)