proposition: Lemma equiv_subst : forall s t, equiv s t -> forall sigma, equiv (apply_subst sigma s) (apply_subst sigma t).
proof: Proof. intros s t; generalize s; clear s. pattern t; apply term_rec3_mem; clear t. intros v s v_eq_s; inversion v_eq_s; subst; intro sigma; apply Eq. intros f l IHl s fl_eq_s sigma; inversion fl_eq_s as [ s' | f' g l1 l2 Sf Sg f'_eq_g l1_eq_l2 | f' g l1 l2 Sf Sg f'_eq_g P ]; subst. apply Eq. simpl; apply Eq_lex; trivial. generalize l1 l1_eq_l2; clear fl_eq_s l1 l1_eq_l2; induction l as [ | s l]; intros l1 l1_eq_l2; inversion l1_eq_l2 as [ | s1 s' l1' l' s1_eq_s' l1'_eq_l']; subst. simpl; apply Eq_list_nil. simpl; apply Eq_list_cons. apply IHl; trivial; left; reflexivity. apply IHl0; trivial. intros t t_in_l; apply IHl; right; trivial. simpl; apply Eq_mul; trivial. apply (permut_map (A := term) (B := term) (A' := term) (B' := term) (R := equiv)). intros a1 a2 a1_in_l1 _ a1_eq_a2; symmetry; apply IHl. rewrite <- (mem_permut0_mem equiv_equiv a1 P). apply in_impl_mem; trivial. intros; apply Eq. symmetry; trivial. trivial. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)