proposition: Lemma R1_at_top_aux_2 : forall t, (forall f, symb_in_term f t = true -> ~defined R2 f) -> forall sigma, Interp_dom R1 R2 (apply_subst sigma t) -> {sigma' : substitution | Interp_subst (var_list t) sigma sigma'}.
proof: Proof. intros t Ct sigma Ht. assert (H : forall v, In v (var_list t) -> {s' : term | Interp_dom R1 R2 (apply_subst sigma (Var v)) /\ Interp (apply_subst sigma (Var v)) s'}). intros v v_in_l; assert (H' := interp_dom_subst R1 R2 t sigma Ht v v_in_l). destruct (interp_defined _ H') as [s' Hs']; exists s'; split; trivial. assert (H' : forall l, (forall v, In v l -> {s' : term | Interp_dom R1 R2 (apply_subst sigma (Var v)) /\ Interp (apply_subst sigma (Var v)) s'}) -> {l' : substitution | Interp_subst l sigma l'}). intro l; induction l as [ | x l]. intros _; exists (nil : substitution); unfold Interp_subst; intros; contradiction. intro H''; destruct IHl as [sigma' Hsigma']. intros v v_in_l; apply H''; right; trivial. destruct (H'' x) as [x' [Hx' Hx'']]. left; trivial. exists ((x,x') :: sigma'). unfold Interp_subst. intros v [v_eq_x | v_in_l]. subst v; simpl; split; trivial. generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _ | intros x_diff_x; absurd (x = x)]; trivial. destruct (Hsigma' v v_in_l) as [H''' H'''']; split; trivial. simpl; generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intros v_eq_x | intros v_diff_x; trivial]. subst v; simpl in Hx'; trivial. destruct (H' _ H) as [sigma' Hsigma']. exists sigma'; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)