proposition: Lemma restrict_var s l x : In x l -> restrict s l x = s x.
proof: Proof. intro. unfold restrict. assert (Inb x l = true). apply Inb_intro. hyp. rewrite H0. refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)