proposition: Lemma sub_sub s1 s2 t : sub s1 (sub s2 t) = sub (sub_comp s1 s2) t.
proof: Proof. set (P := fun t => sub s1 (sub s2 t) = sub (sub_comp s1 s2) t). change (P t). apply term_ind_forall with (P := P); intros; unfold P. refl. simpl. f_equal. rewrite Vmap_map. apply Vmap_eq. hyp. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)