proposition: Lemma decompose_subst_aux : forall s1 s2 sigma, well_formed s1 -> well_formed s2-> (forall x u, In (x,u) sigma -> match u with | Var _ => True | Term f l => (match F.arity f with Free n => n | _ => 2 end) <> length l end) -> (forall x u v, In (x,u) sigma -> In (x,v) sigma -> u = v) -> (forall x y u, In (x,u) sigma -> In (y,u) sigma -> x = y) -> (forall x, In x (var_list s1) -> In x (map (@fst _ _) sigma)) -> (forall x, In x (var_list s2) -> In x (map (@fst _ _) sigma)) -> apply_subst sigma s1 = apply_subst sigma s2 -> s1 = s2.
proof: Proof. intro s1; pattern s1; apply term_rec3; clear s1. intros v1 [v2 | f2 l2] sigma W1 W2 H1 H2 H3 H41 H42 H0. apply f_equal; apply H3 with (apply_subst sigma (Var v1)). assert (v1_in_sig : In v1 (map (@fst _ _) sigma)). apply H41; left; apply eq_refl. rewrite in_map_iff in v1_in_sig; destruct v1_in_sig as [[v1' u1] [v1_eq_v1' v1_in_sig]]; simpl in v1_eq_v1'; subst v1'. simpl; rewrite (subst_aux _ H2 _ _ v1_in_sig); assumption. rewrite H0; assert (v2_in_sig : In v2 (map (@fst _ _) sigma)). apply H42; left; apply eq_refl. rewrite in_map_iff in v2_in_sig; destruct v2_in_sig as [[v2' u1] [v2_eq_v2' v2_in_sig]]; simpl in v2_eq_v2'; subst v2'. simpl; rewrite (subst_aux _ H2 _ _ v2_in_sig); assumption. assert (v1_in_sig : In v1 (map (@fst _ _) sigma)). apply H41; left; apply eq_refl. rewrite in_map_iff in v1_in_sig; destruct v1_in_sig as [[v1' u1] [v1_eq_v1' v1_in_sig]]; simpl in v1_eq_v1'; subst v1'. simpl in H0; rewrite (subst_aux _ H2 _ _ v1_in_sig) in H0. destruct u1 as [x1 | g1 k1]. discriminate. apply False_rect; apply (H1 _ _ v1_in_sig). injection H0; clear H0; do 2 intro; subst g1 k1; rewrite map_length; apply sym_eq. destruct (well_formed_unfold W2) as [_ L2]; destruct (F.arity f2); assumption. intros f1 l1 Hl1 [v2 | f2 l2] sigma W1 W2 H1 H2 H3 H41 H42 H0. assert (v2_in_sig : In v2 (map (@fst _ _) sigma)). apply H42; left; apply eq_refl. rewrite in_map_iff in v2_in_sig; destruct v2_in_sig as [[v2' u2] [v2_eq_v2' v2_in_sig]]; simpl in v2_eq_v2'; subst v2'. simpl in H0; rewrite (subst_aux _ H2 _ _ v2_in_sig) in H0. destruct u2 as [x2 | g2 k2]. discriminate. apply False_rect; apply (H1 _ _ v2_in_sig). injection H0; clear H0; do 2 intro; subst g2 k2; rewrite map_length; apply sym_eq. destruct (well_formed_unfold W1) as [_ L1]; destruct (F.arity f1); assumption. simpl in H0; injection H0; clear H0; intro H0; intro; subst f2; apply f_equal. rewrite var_list_unfold in H41, H42. destruct (well_formed_unfold W1) as [Wl1 _]; clear W1. destruct (well_formed_unfold W2) as [Wl2 _]; clear W2. revert l2 sigma Wl1 Wl2 H1 H2 H3 H41 H42 H0. induction l1 as [ | t1 l1]; intros [ | t2 l2] sigma Wl1 Wl2 H1 H2 H3 H41 H42 H0. apply eq_refl. discriminate. discriminate. simpl in H0; injection H0; clear H0; intros H0 h0. rewrite (Hl1 t1 (or_introl _ (eq_refl _)) t2 sigma); trivial. apply f_equal; rewrite (IHl1 (tail_prop _ Hl1) l2 sigma); trivial. intros u u_in_l1; apply Wl1; right; assumption. intros u u_in_l2; apply Wl2; right; assumption. intros v v_in_l1; apply H41; apply in_or_app; right; assumption. intros v v_in_l2; apply H42; apply in_or_app; right; assumption. apply Wl1; left; apply eq_refl. apply Wl2; left; apply eq_refl. intros v v_in_t1; apply H41; apply in_or_app; left; assumption. intros v v_in_t2; apply H42; apply in_or_app; left; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)