proposition: Lemma dom_incl_restrict s l : dom_incl (restrict s l) l.
proof: Proof. unfold dom_incl. intros. ded (Inb_elim eq_nat_dec _ _ H). unfold restrict. rewrite H0. refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)