proposition: Lemma Lge_Decr : forall f (ts : terms' (arity f)) (a b : L f), a >=L b -> red Decr # (Fun' (mk a) ts) (Fun' (mk b) ts).
proof: Proof. intros. destruct H. subst. apply rt_refl. apply rt_step. exists (Fun'_vars a). exists (Fun'_vars b). exists Hole. exists (sub_vars ts). simpl. intuition. exists f. exists a. exists b. intuition. apply args_eq. apply sub_fresh_vars. apply args_eq. apply sub_fresh_vars. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)