proposition: Lemma cc_succeq : context_closed succeq.
proof: Proof. intros t u c [h|h]. left. apply cc_succ. hyp. right. apply cc_equiv_aterm. 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)