proposition: Lemma lt_subst_closed : substitution_closed lt.
proof: Proof. intros p q. gen p. clear p. pattern q. apply well_founded_ind with term (@subterm Sig). apply subterm_wf. clear q. intros q IH p. gen IH. clear IH. pattern p. apply well_founded_ind with term (@subterm Sig). apply subterm_wf. clear p. intros p IH IH'. destruct q. intros. exfalso. eapply var_are_min. eexact H. intros. lt_inversion H. subst p. simpl. apply lt_roots. replace f with g. hyp. congruence. intros. rewrite <- sub_fun. destruct (proj1 (in_map_iff (sub s) ss t)) as [t' [t't t'ss]]. hyp. subst t. apply IH. apply subterm_immediate. hyp. hyp. rewrite t_is. apply Hsub. hyp. subst p. do 2 rewrite sub_fun. apply lt_status. apply eqF_sym. replace f with g. hyp. congruence. intros. rewrite <- sub_fun. destruct (proj1 (in_map_iff (sub s) ss t)) as [t' [t't t'ss]]. hyp. subst t. apply IH. apply subterm_immediate. hyp. hyp. rewrite t_is. apply Hsub. hyp. replace f with g; [rewrite <- (status_eq f0 g eqFfg) | congruence]. apply status_homomorphic. intros. apply IH'. apply subterm_immediate. hyp. hyp. congruence. rewrite sub_fun. apply lt_subterm. exists (sub s t'). split. apply (proj2 (in_map_iff (sub s) l (sub s t'))). exists t'. split. refl. replace l with ts. hyp. congruence. destruct Ht'. left. congruence. right. apply IH'. apply subterm_immediate. replace l with ts. hyp. congruence. hyp. Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)