proposition: Lemma proj_sub_fun : forall s f ts, proj (sub s (Fun f ts)) = sub s (proj (Fun f ts)).
proof: Proof. intros. simpl. case (zerop (arity f)). intros. simpl. refl. intros. rewrite Vnth_map; auto. Qed.
imports: CoLoR(ATrs NatUtil BoolUtil VecUtil ListUtil LogicUtil RelUtil SN ACompat ARelation EqUtil)