proposition: Lemma subc_cont : forall s (c : context), subc s c = c.
proof: Proof. induction c; simpl; intros. refl. arity. simpl. rewrite IHc. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)