proposition: Lemma sub_eq_restrict s : forall l, sub_eq_dom (restrict s l) s l.
proof: Proof. unfold sub_eq_dom, restrict. induction l; simpl. intros. contr. intro. case (eq_nat_dec x a); intuition. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)