proposition: Lemma proj_sub_var : forall s n, proj (sub s (Var n)) = sub (proj_sub s) (Var n).
proof: Proof. intros. simpl. auto. Qed.
imports: CoLoR(ATrs NatUtil BoolUtil VecUtil ListUtil LogicUtil RelUtil SN ACompat ARelation EqUtil)