proposition: Lemma sc_succeq : substitution_closed succeq.
proof: Proof. intros t u s [h|h]. left. apply sc_succ. hyp. right. unfold equiv_aterm, Rof. set (k := max (maxvar t) (maxvar u)). rewrite term_of_aterm_sub with (k:=S k). 2: apply le_n_S; apply Nat.le_max_l. rewrite term_of_aterm_sub with (k:=S k). 2: apply le_n_S; apply Nat.le_max_r. apply equiv_subst. hyp. Qed.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil) CoLoR(NatUtil) Coq(List Relations) CoLoR(term SN ASubstitution) CoLoR(rpo rpo_extension) CoLoR(ARedPair ARelation RelUtil BoolUtil)