proposition: Lemma clos_aeq_tc_supterm_acc_subs : forall s t u, clos_aeq (supterm_acc!) t u -> clos_aeq (supterm_acc!) (subs s t) (subs s u).
proof: Proof. intros s t u tu. destruct (clos_aeq_inv tu) as [t' [u' [tt' [uu' t'u']]]]; clear tu. rewrite tt', uu'. apply clos_aeq_intro_refl. apply tc_supterm_acc_subs. hyp. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)