proposition: Lemma sub_fill s u : forall C, sub s (fill C u) = fill (subc s C) (sub s u).
proof: Proof. induction C; intros. refl. simpl subc. simpl fill. simpl sub. f_equal. rewrite Vmap_cast, Vmap_app. simpl Vmap. rewrite IHC. refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)