proposition: Lemma proj_sub : forall s t, proj (sub s t) = sub (psub s) (proj t).
proof: Proof. intro. apply term_ind_forall; intros. refl. simpl. case (pi f). intros [k h]. rewrite Vnth_map. apply Vforall_nth. hyp. simpl. apply args_eq. rewrite !Vmap_map. apply Vmap_eq. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil SN ARelation RelUtil ACompat NatUtil)