proposition: Lemma red_ren : forall t u, red R (sub s t) u -> exists v, red R t v /\ sub s v = u.
proof: Proof. intros t u. rewrite red1_ok. 2: hyp. intro h. destruct h as [l]. destruct H as[r]. destruct H as [c]. destruct H as [d]. decomp H. exists (fill (comp c (comp (cont r) d)) (Var (var t))). rewrite red1_ok. 2: hyp. split. ex l r c d. split_all. revert H2. rewrite (term_cont_var t), sub_fill, !var_fill. simpl. rewrite subc_cont. destruct (hs (var t)). rewrite H. simpl. intro. destruct (fill_var_elim H2) as [e]. revert H2. rewrite H1, !comp_comp. intro. rewrite fill_eq_cont, !comp_eq in H2. rewrite H2. refl. rewrite sub_fill, subc_cont, H3, fill_eq. simpl. rewrite var_sub. destruct (hs (var t)). rewrite H. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)