proposition: Lemma red_sub_ren_cap : forall u v, red R u v -> forall k, exists s, v = sub s (ren_cap k u).
proof: Proof. intros u v H. redtac. subst. elim c; clear c; simpl; intros. destruct l. is_var_lhs. assert (defined f R = true). eapply lhs_fun_defined. apply lr. rewrite sub_fun, ren_cap_fun, H. exists_single k (sub s r). rewrite ren_cap_fun. case (defined f R). simpl. exists_single k (Fun f (Vcast (Vapp t (Vcons (fill c (sub s r)) t0)) e)). rewrite ren_caps_cast, ren_caps_app. simpl ren_caps. destruct (ren_caps_intro t k) as [s1]. destruct H0 as [H0 H0']. destruct (H (k + nb_aliens_vec t)) as [s2]. destruct (ren_caps_intro t0 (k + nb_aliens_vec t + nb_aliens (fill c (sub s l)))) as [s3]. destruct H2 as [H2 H2']. set (s' := fun x => match In_dec x (vars_vec (ren_caps k t)) with | left _ => s1 x | right _ => match In_dec x (vars (ren_cap (k + nb_aliens_vec t) (fill c (sub s l)))) with | left _ => s2 x | right _ => s3 x end end). exists s'. rewrite sub_fun. apply args_eq. rewrite Vmap_cast, Vmap_app. simpl. apply Vcast_eq_intro. apply Vapp_eq_intro. trans (Vmap (sub s1) (ren_caps k t)). hyp. apply Vmap_sub_eq. intros. ded (vars_ren_caps H3). unfold s'. case (In_dec x (vars_vec (ren_caps k t))); intro. refl. intuition. apply Vcons_eq_intro. rewrite H1. apply sub_eq. intros. ded (vars_ren_cap H3). unfold s'. case (In_dec x (vars_vec (ren_caps k t))); intro. ded (vars_ren_caps i0). lia. case (In_dec x (vars (ren_cap (k + nb_aliens_vec t) (fill c (sub s l))))); intro. refl. intuition. trans (Vmap (sub s3) (ren_caps (k + nb_aliens_vec t + nb_aliens (fill c (sub s l))) t0)). hyp. apply Vmap_sub_eq. intros. ded (vars_ren_caps H3). unfold s'. case (In_dec x (vars_vec (ren_caps k t))); intro. ded (vars_ren_caps i0). lia. case (In_dec x (vars (ren_cap (k + nb_aliens_vec t) (fill c (sub s l))))); intro. ded (vars_ren_cap i0). lia. refl. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)