proposition: Lemma red_lab : forall v t u, red R t u -> red_mod Decr R' (lab v t) (lab v u).
proof: Proof. intros. redtac. subst. elim c; clear c. simpl. exists (lab v (sub s l)). split. apply rt_refl. rewrite !lab_sub_eq. exists (lab (beta v s) l). exists (lab (beta v s) r). exists Hole. exists (lab_sub v s). intuition. exists (mkRule l r). exists (beta v s). intuition. intros. simpl. rewrite !Vmap_cast, !Vmap_app. simpl. set (v0' := Vmap (int v) t). set (l1 := fill c (sub s l)). fold l1 in H. set (v1' := Vmap (int v) t0). set (r1 := fill c (sub s r)). fold r1 in H. assert (int v l1 >=D int v r1). assert (IR I Dge l1 r1). apply IR_context_closed. hyp. apply IR_substitution_closed. apply ge_compat. hyp. apply H0. set (a := pi f (Vcast (Vapp v0' (Vcons (int v l1) v1')) e)). set (b := pi f (Vcast (Vapp v0' (Vcons (int v r1) v1')) e)). assert (a >=L b). apply pi_mon. hyp. set (w0 := Vmap (lab v) t). set (w1 := Vmap (lab v) t0). set (ts := Vcast (Vapp w0 (Vcons (lab v l1) w1)) e). ded (Lge_Decr ts H1). set (us := Vcast (Vapp w0 (Vcons (lab v r1) w1)) e). do 2 destruct H. set (vs := Vcast (Vapp w0 (Vcons x w1)) e). exists (Fun' (mk b) vs). split. apply rt_trans with (Fun' (mk b) ts). hyp. apply context_closed_fun with (R := red Decr #). apply context_closed_rtc. apply context_closed_red. hyp. apply context_closed_fun with (R := red R'). apply context_closed_red. hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)