proposition: Lemma afs_subst : forall t sigma, afs (M.apply_subst sigma t) = M.apply_subst (sigma_afs sigma) (afs t).
proof: Proof. intros; pattern t; apply M.term_rec3; intros. induction sigma as [|[v0 t0] sigma]; [ reflexivity |]; simpl; case (M.eq_var_bool v v0); [ reflexivity | assumption ]. unfold afs; simpl; destruct (afs_symb f) as [g ns]; simpl; f_equal; clear f g. rewrite map_length; rewrite map_length; rewrite map_length; set (ns0 := afs_rest ns ns (length l)); clearbody ns0; clear ns. revert l H; induction ns0 as [|i ns]; intros; [ reflexivity |]. cut( (nth_error (map afs (map (M.apply_subst sigma) l)) i = None /\ nth_error (map afs l) i = None) \/ (exists t0, exists t1, nth_error (map afs (map (M.apply_subst sigma) l)) i = Some t0 /\ nth_error (map afs l) i = Some t1 /\ t0 = M.apply_subst (sigma_afs sigma) t1)); [ intros [[H0 H1]|[t0 [t1 [H0 [H1 H2]]]]]; simpl; unfold afs in *; rewrite H0; rewrite H1; [| simpl; f_equal; [ assumption |]]; apply IHns; assumption |]. revert i; induction l as [|s l]; [ left; destruct i; split; reflexivity | destruct i ]; [| simpl; apply IHl; intros; apply H; right; assumption ]; right; exists (afs (M.apply_subst sigma s)); exists (afs s); split; [ reflexivity |]; split; [ reflexivity |]; apply H; left; reflexivity. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)