proposition: Lemma proj_subs_closed : substitution_closed succ -> substitution_closed psucc.
proof: Proof. unfold substitution_closed. intros. unfold proj_ord. rewrite !proj_sub. apply H. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil SN ARelation RelUtil ACompat NatUtil)