proposition: Lemma equiv_add_context : forall p ctx s t, equiv s t -> is_a_pos ctx p = true -> equiv (replace_at_pos ctx s p) (replace_at_pos ctx t p).
proof: Proof. intro p; induction p as [ | i p ]; intros ctx s t R H; trivial; destruct ctx as [ v | f l ]. discriminate. assert (Status : forall g, g = f -> status Prec g = status Prec f). intros; subst; trivial. do 2 (rewrite replace_at_pos_unfold); destruct (status Prec f); generalize (Status f (eq_refl _)); clear Status; intro Status. apply Eq_lex; trivial. apply prec_eq_refl. generalize i H; clear i H; induction l as [ | u l]; intros i H; simpl. apply Eq_list_nil. destruct i as [ | i]. apply Eq_list_cons. simpl in H; apply IHp; trivial. generalize l; intro l'; induction l' as [ | u' l']. apply Eq_list_nil. apply Eq_list_cons; trivial; reflexivity. apply Eq_list_cons. reflexivity. apply IHl; trivial. apply Eq_mul; trivial. apply prec_eq_refl. generalize i H; clear i H; induction l as [ | u l]; intros i H; simpl; reflexivity || auto. destruct i as [ | i]. rewrite <- permut0_cons. reflexivity. apply equiv_equiv. simpl in H; apply IHp; trivial. rewrite <- permut0_cons. apply IHl; trivial. apply equiv_equiv. reflexivity. 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)