Click on a command or tactic to see a detailed view of its use.
Specification "trans". Import "typing". [View typing] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%% Source language substitutions with no duplications %%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Substitutions Define ssubst : smap_list -> prop by ssubst smnil; nabla x, ssubst (smcons (smap x V) ML) := ssubst ML /\ {val V} /\ {tm V}. Define vars_of_ssubst : smap_list -> tm_list -> prop by vars_of_ssubst smnil snil; nabla x, vars_of_ssubst (smcons (smap x V) ML) (scons x L) := vars_of_ssubst ML L. % Application of substitutions Define app_ssubst : smap_list -> tm -> tm -> prop by app_ssubst smnil M M; nabla x, app_ssubst (smcons (smap x V) ML) (R x) M := app_ssubst ML (R V) M. % Lemmas of substitutions Theorem app_ssubst_exists: forall ML M, ssubst ML -> exists M', app_ssubst ML M M'. Theorem ssubst_det : forall ML M M' M'', ssubst ML -> app_ssubst ML M M' -> app_ssubst ML M M'' -> M' = M''.induction on 1. intros. case H1. case H2. case H3. search. case H2. case H3. apply IH to H4 H7 H8. search.Theorem ssubst_closed_tm_eq : forall M ML M', {tm M} -> app_ssubst ML M M' -> M = M'. Theorem ssubst_inst : forall ML M M' V, nabla (x:tm), {tm V} -> app_ssubst ML (M x) (M' x) -> app_ssubst ML (M V) (M' V).induction on 2. intros. case H2. search. apply sclosed_tm_prune to H1. unfold. intros. apply IH to H1 H3. search.Theorem explct_meta_ssubst_comm : forall ML M E V, nabla n, {tm V} -> app_ssubst ML (M n) (E n) -> app_ssubst (smcons (smap n V) ML) (M n) (E V). Theorem ssubst_closed_tm : forall M ML, {tm M} -> ssubst ML -> app_ssubst ML M M. Theorem ssubst_var : forall V ML X, ssubst ML -> smmember (smap X V) ML -> app_ssubst ML X V.induction on 2. intros. case H2. case H1. unfold. backchain ssubst_closed_tm. case H1. apply smmember_prune_tm to H3. unfold. backchain IH.Theorem ssubst_var_eq : forall V ML E X, ssubst ML -> smmember (smap X V) ML -> app_ssubst ML X E -> E = V. Theorem ssubst_nabla : forall ML, nabla (x:tm), ssubst ML -> app_ssubst ML x x. Theorem ssubst_result_closed_tm : forall ML L M M' Vs, tm_sctx L -> {L |- tm M} -> vars_of_tm_sctx L Vs -> ssubst ML -> vars_of_ssubst ML Vs -> app_ssubst ML M M' -> {tm M'}.induction on 1. intros. case H1. case H3. case H5. case H6. search. case H3. case H5. case H6. case H4. inst H2 with n1 = V. cut H14 with H13. backchain IH with ML = ML1, L = L1, M = (M V).Theorem ssubst_result_closed_tm' : forall ML L T M M' Vs, {is_sty T} -> sctx L -> {L |- of M T} -> vars_of_sctx L Vs -> ssubst ML -> vars_of_ssubst ML Vs -> app_ssubst ML M M' -> {tm M'}.intros. apply sctx_to_tm_sctx to H2 H4. assert {SL |- tm M}. backchain sof_to_tm with T = T. backchain ssubst_result_closed_tm.% Commutative property of applications of substitions Theorem app_ssubst_pred_comm : forall ML M M', app_ssubst ML (pred M) M' -> exists M'', M' = pred M'' /\ app_ssubst ML M M''. Theorem app_ssubst_ifz_comm : forall ML M M1 M2 M3, app_ssubst ML (ifz M M1 M2) M3 -> exists M' M1' M2', M3 = ifz M' M1' M2' /\ app_ssubst ML M M' /\ app_ssubst ML M1 M1' /\ app_ssubst ML M2 M2'. Theorem app_ssubst_let_comm : forall ML M R M', app_ssubst ML (let M R) M' -> exists M1 R1, M' = let M1 R1 /\ app_ssubst ML M M1 /\ nabla x, app_ssubst ML (R x) (R1 x). Theorem app_ssubst_fix_comm : forall ML R M', app_ssubst ML (fix R) M' -> exists R', M' = fix R' /\ nabla f x, app_ssubst ML (R f x) (R' f x). Theorem app_ssubst_app_comm : forall ML M1 M2 M', app_ssubst ML (app M1 M2) M' -> exists M1' M2', M' = app M1' M2' /\ app_ssubst ML M1 M1' /\ app_ssubst ML M2 M2'. Theorem app_ssubst_plus_comm : forall ML M1 M2 M', app_ssubst ML (plus M1 M2) M' -> exists M1' M2', M' = plus M1' M2' /\ app_ssubst ML M1 M1' /\ app_ssubst ML M2 M2'. Theorem app_ssubst_pair_comm : forall ML M1 M2 M', app_ssubst ML (pair M1 M2) M' -> exists M1' M2', M' = pair M1' M2' /\ app_ssubst ML M1 M1' /\ app_ssubst ML M2 M2'. Theorem app_ssubst_fst_comm : forall ML M M', app_ssubst ML (fst M) M' -> exists M1', M' = fst M1' /\ app_ssubst ML M M1'. Theorem app_ssubst_snd_comm : forall ML M M', app_ssubst ML (snd M) M' -> exists M1', M' = snd M1' /\ app_ssubst ML M M1'. Theorem app_ssubst_meta_app_comm : forall ML R (M:tm) P, app_ssubst ML (R M) P -> exists R' M', P = R' M' /\ app_ssubst ML M M' /\ nabla x, app_ssubst ML (R x) (R' x).induction on 1. intros. case H1. exists R. exists M. search. apply IH to H2 with R = R V, M = M V. exists R'. exists M'. search.% Composition of substitution applications Theorem app_ssubst_pred_compose : forall ML M M', app_ssubst ML M M' -> app_ssubst ML (pred M) (pred M'). Theorem app_ssubst_ifz_compose : forall ML M1 M2 M1' M2' M3 M3', app_ssubst ML M1 M1' -> app_ssubst ML M2 M2' -> app_ssubst ML M3 M3' -> app_ssubst ML (ifz M1 M2 M3) (ifz M1' M2' M3'). Theorem app_ssubst_plus_compose : forall ML M1 M2 M1' M2', app_ssubst ML M1 M1' -> app_ssubst ML M2 M2' -> app_ssubst ML (plus M1 M2) (plus M1' M2'). Theorem app_ssubst_fst_compose : forall ML M M', app_ssubst ML M M' -> app_ssubst ML (fst M) (fst M'). Theorem app_ssubst_snd_compose : forall ML M M', app_ssubst ML M M' -> app_ssubst ML (snd M) (snd M'). Theorem app_ssubst_pair_compose : forall ML M1 M2 M1' M2', app_ssubst ML M1 M1' -> app_ssubst ML M2 M2' -> app_ssubst ML (pair M1 M2) (pair M1' M2'). Theorem app_ssubst_app_compose : forall ML M1 M2 M1' M2', app_ssubst ML M1 M1' -> app_ssubst ML M2 M2' -> app_ssubst ML (app M1 M2) (app M1' M2'). Theorem app_ssubst_fix_compose : forall ML M M', nabla f x, app_ssubst ML (M f x) (M' f x) -> app_ssubst ML (fix M) (fix M').induction on 1. intros. case H1. search. unfold. backchain IH with M = M ML2, M' = M2, f = n1, x = n2.Theorem app_ssubst_let_compose : forall ML M1 M2 M1' M2', nabla x, app_ssubst ML M1 M1' -> app_ssubst ML (M2 x) (M2' x) -> app_ssubst ML (let M1 M2) (let M1' M2'). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%% Source language substitutions with duplications %%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Explicit source substitutions Define subst : smap_list -> prop by subst smnil; subst (smcons (smap X V) ML) := subst ML /\ name X /\ {val V} /\ {tm V} /\ forall V', smmember (smap X V') ML -> V' = V. % Application of the source substitutions Define app_subst : smap_list -> tm -> tm -> prop by app_subst smnil M M; nabla x, app_subst (smcons (smap x V) (ML x)) (R x) M := nabla x, app_subst (ML x) (R V) M. % Lemmas about substitutions Theorem subst_mem : forall ML E, subst ML -> smmember E ML -> exists X V, E = smap X V /\ name X /\ {val V} /\ {tm V}. Theorem subst_extend : forall ML V, nabla x, subst ML -> {tm V} -> {val V} -> subst (smcons (smap x V) ML). Theorem subst_var_rsl_clear : forall ML V M M', nabla x, subst (ML x) -> smmember (smap x V) (ML x) -> app_subst (ML x) (M x) (M' x) -> exists M'', M' = y\M''.induction on 2. intros. case H2. case H3. search. case H3. % The head of (ML x) is not x case H1. apply closed_tm_prune to H9. apply IH to H6 H4 H5. search. % The head of (ML x) is x search.Theorem subst_var_inst : forall ML V M M', nabla x, subst (ML x) -> smmember (smap x V) (ML x) -> app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'.induction on 2. intros. apply subst_mem to H1 H2. case H2. unfold. intros. case H3. search. case H3 (keep). % The head of (ML x) is not x case H1. apply closed_tm_prune to H6. apply closed_tm_prune to H12. apply IH to H9 H7 H8. search. % The head of (ML x) is x case H1. apply H13 to H7. search.Theorem subst_det : forall ML M M' M'', subst ML -> app_subst ML M M' -> app_subst ML M M'' -> M' = M''.induction on 1. intros. case H1. case H2. case H3. search. case H2. case H3. apply IH to H4 H9 H10. search.Theorem subst_closed_tm_eq : forall M ML M', {tm M} -> app_subst ML M M' -> M = M'. Theorem subst_closed_tm : forall M ML, {tm M} -> subst ML -> app_subst ML M M.induction on 2. intros. case H2. search. case H4. apply closed_tm_prune to H1. apply closed_tm_prune to H6. apply IH to H1 H3. search.Theorem subst_var : forall V ML X, subst ML -> smmember (smap X V) ML -> app_subst ML X V.induction on 2. intros. case H2. case H1. case H4. apply closed_tm_prune to H6. unfold. intros. backchain subst_closed_tm. case H1. apply subst_mem to H4 H3. case H9. apply closed_tm_prune to H11. apply closed_tm_prune to H7. case H5. % The head of ML is not X apply closed_tm_prune to H11. apply closed_tm_prune to H7. apply IH to H4 H3. search. % The head of ML is X apply H8 to H3. unfold. intros. backchain subst_closed_tm.Theorem subst_var_eq : forall V ML E X, subst ML -> smmember (smap X V) ML -> app_subst ML X E -> E = V. Theorem subst_inst : forall ML M M' V, nabla (x:tm), {tm V} -> app_subst ML (M x) (M' x) -> app_subst ML (M V) (M' V).induction on 2. intros. case H2. search. apply closed_tm_prune to H1. unfold. intros. apply IH to H1 H3. search.Theorem explct_meta_subst_comm : forall ML M E V, nabla n, {tm V} -> app_subst ML (M n) (E n) -> app_subst (smcons (smap n V) ML) (M n) (E V). Define vars_in_subst : tm_list -> smap_list -> prop by vars_in_subst snil ML; vars_in_subst (scons X Vs) ML := vars_in_subst Vs ML /\ exists V, smmember (smap X V) ML. Theorem vars_in_subst_extend : forall Vs L E, vars_in_subst Vs L -> vars_in_subst Vs (smcons E L). Theorem subst_result_closed_tm : forall ML L M M' Vs, subst ML -> tm_ctx L -> {L |- tm M} -> vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' -> {tm M'}.induction on 2. intros. case H2. case H4. case H5. apply subst_closed_tm_eq to _ H6. search. case H4. case H5. apply subst_mem to _ H11. case H8. apply closed_tm_prune to H14. apply tm_cut to _ H7 H3. apply subst_var_rsl_clear to _ H11 H6. apply subst_var_inst to _ H11 H6. apply IH to H1 H7 H15 _ _ H16. search.% Commutative property of applications of substitions Theorem app_subst_pred_comm : forall ML M M', app_subst ML (pred M) M' -> exists M'', M' = pred M'' /\ app_subst ML M M''. Theorem app_subst_ifz_comm : forall ML M M1 M2 M3, app_subst ML (ifz M M1 M2) M3 -> exists M' M1' M2', M3 = ifz M' M1' M2' /\ app_subst ML M M' /\ app_subst ML M1 M1' /\ app_subst ML M2 M2'. Theorem app_subst_let_comm : forall ML M R M', app_subst ML (let M R) M' -> exists M1 R1, M' = let M1 R1 /\ app_subst ML M M1 /\ nabla x, app_subst ML (R x) (R1 x). Theorem app_subst_fix_comm : forall ML R M', app_subst ML (fix R) M' -> exists R', M' = fix R' /\ nabla f x, app_subst ML (R f x) (R' f x). Theorem app_subst_app_comm : forall ML M1 M2 M', app_subst ML (app M1 M2) M' -> exists M1' M2', M' = app M1' M2' /\ app_subst ML M1 M1' /\ app_subst ML M2 M2'. Theorem app_subst_plus_comm : forall ML M1 M2 M', app_subst ML (plus M1 M2) M' -> exists M1' M2', M' = plus M1' M2' /\ app_subst ML M1 M1' /\ app_subst ML M2 M2'. Theorem app_subst_pair_comm : forall ML M1 M2 M', app_subst ML (pair M1 M2) M' -> exists M1' M2', M' = pair M1' M2' /\ app_subst ML M1 M1' /\ app_subst ML M2 M2'. Theorem app_subst_fst_comm : forall ML M M', app_subst ML (fst M) M' -> exists M1', M' = fst M1' /\ app_subst ML M M1'. Theorem app_subst_snd_comm : forall ML M M', app_subst ML (snd M) M' -> exists M1', M' = snd M1' /\ app_subst ML M M1'. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%% Target language substitutions with no duplications %%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Explicit target substitutions Define subst' : cmap_list -> prop by subst' cmnil; nabla x, subst' (cmcons (cmap x V) ML) := subst' ML /\ {val' V} /\ {tm' V}. Define vars_of_subst' : cmap_list -> tm'_list -> prop by vars_of_subst' cmnil cnil; nabla x, vars_of_subst' (cmcons (cmap x V) ML) (ccons x L) := vars_of_subst' ML L. % Application of the targt substitutions Define app_subst' : cmap_list -> tm' -> tm' -> prop by app_subst' cmnil M M; nabla x, app_subst' (cmcons (cmap x V) ML) (R x) M := app_subst' ML (R V) M. Theorem app_subst'_exists: forall ML M, subst' ML -> exists M', app_subst' ML M M'. % Application of substitutions to a list of tm' terms Define app_subst'_list : cmap_list -> tm'_list -> tm'_list -> prop by app_subst'_list cmnil L L; nabla x, app_subst'_list (cmcons (cmap x V) ML) (L x) L' := app_subst'_list ML (L V) L'. Theorem app_subst'_islist : forall L L' ML, is_tm'_list L -> app_subst'_list ML L L' -> is_tm'_list L'.induction on 2. intros. case H2. search. apply is_tm'_list_inst to H1 with V = V. apply IH to H4 H3. search.% Lemmas about substitutions Theorem subst'_nabla : forall ML, nabla (x:tm'), subst' ML -> app_subst' ML x x. Theorem subst'_result_closed_tm : forall ML L M M' Vs, tm'_ctx L -> {L |- tm' M} -> vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs -> app_subst' ML M M' -> {tm' M'}.induction on 1. intros. case H1. case H3. case H5. case H6. search. case H3. case H5. case H6. case H4. inst H2 with n1 = V. cut H14 with H13. backchain IH with ML = ML1, L = L1, M = (M V).Theorem subst'_result_closed_tm'' : forall ML L M M' Vs, tm'_ctx L -> {L |- tm'' M} -> vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs -> app_subst' ML M M' -> {tm'' M'}.induction on 1. intros. case H1. case H3. case H5. case H6. search. case H3. case H5. case H6. case H4. inst H2 with n1 = V. cut H14 with H13. backchain IH with ML = ML1, L = L1, M = (M V).Theorem app_subst'_prune : forall ML M M', nabla (x:tm'), app_subst' ML M (M' x) -> exists M'', M' = y\M''. Theorem subst'_mem : forall ML E, subst' ML -> cmmember E ML -> exists X V, E = cmap X V /\ name' X /\ {val' V} /\ {tm' V}. Theorem subst'_extend : forall ML V, nabla x, subst' ML -> {tm' V} -> {val' V} -> subst' (cmcons (cmap x V) ML). Theorem subst'_closed_tm_eq : forall M ML M', {tm' M} -> app_subst' ML M M' -> M = M'. Theorem subst'_closed_tm : forall M ML, {tm' M} -> subst' ML -> app_subst' ML M M. Theorem subst'_det : forall ML M M' M'', app_subst' ML M M' -> app_subst' ML M M'' -> M' = M''. Theorem subst'_var : forall V ML X, subst' ML -> cmmember (cmap X V) ML -> app_subst' ML X V.induction on 2. intros. case H2. case H1. unfold. intros. backchain subst'_closed_tm. case H1. apply cmmember_prune_tm' to H3. unfold. intros. backchain IH.Theorem subst'_var_eq : forall V ML E X, subst' ML -> cmmember (cmap X V) ML -> app_subst' ML X E -> E = V. Theorem subst'_inst : forall ML M M' V, nabla (x:tm'), {tm' V} -> app_subst' ML (M x) (M' x) -> app_subst' ML (M V) (M' V).induction on 2. intros. case H2. search. apply closed_tm'_prune to H1. unfold. apply IH to H1 H3. search.Theorem explct_meta_subst'_comm : forall ML M E V, nabla n, {tm' V} -> app_subst' ML (M n) (E n) -> app_subst' (cmcons (cmap n V) ML) (M n) (E V). Theorem subst'_general_inst : forall ML M1 M2 M1' M2', nabla (x:tm'), app_subst' ML M1 M1' -> app_subst' ML (M2 x) (M2' x) -> app_subst' ML (M2 M1) (M2' M1'). %% lemmas for hoisted terms Theorem subst'_closed_tm''_eq : forall M ML M', {tm'' M} -> app_subst' ML M M' -> M = M'. Theorem subst'_closed_tm''_body_eq : forall M ML M', {tm''_body M} -> app_subst' ML M M' -> M = M'.induction on 2. intros. case H2. search. apply closed_tm''_body_prune to H1. apply IH to _ H3. search.% Commutative property of applications of substitions Theorem app_subst'_pred_comm : forall ML M M', app_subst' ML (pred' M) M' -> exists M'', M' = pred' M'' /\ app_subst' ML M M''. Theorem app_subst'_ifz_comm : forall ML M M1 M2 M3, app_subst' ML (ifz' M M1 M2) M3 -> exists M' M1' M2', M3 = ifz' M' M1' M2' /\ app_subst' ML M M' /\ app_subst' ML M1 M1' /\ app_subst' ML M2 M2'. Theorem app_subst'_let_comm : forall ML M R M', app_subst' ML (let' M R) M' -> exists M1 R1, M' = let' M1 R1 /\ app_subst' ML M M1 /\ nabla x, app_subst' ML (R x) (R1 x). Theorem app_subst'_clos_comm : forall ML F M M', app_subst' ML (clos' F M) M' -> exists F' M1', M' = (clos' F' M1') /\ app_subst' ML F F' /\ app_subst' ML M M1'. Theorem app_subst'_open_comm : forall ML M1 M2 M', app_subst' ML (open' M1 (f\e\ app' f (pair' M1 (pair' M2 e)))) M' -> exists M1' M2', M' = (open' M1' (f\e\ app' f (pair' M1' (pair' M2' e)))) /\ app_subst' ML M1 M1' /\ app_subst' ML M2 M2'. Theorem app_subst'_plus_comm : forall ML M1 M2 M', app_subst' ML (plus' M1 M2) M' -> exists M1' M2', M' = plus' M1' M2' /\ app_subst' ML M1 M1' /\ app_subst' ML M2 M2'. Theorem app_subst'_pair_comm : forall ML M1 M2 M', app_subst' ML (pair' M1 M2) M' -> exists M1' M2', M' = pair' M1' M2' /\ app_subst' ML M1 M1' /\ app_subst' ML M2 M2'. Theorem app_subst'_fst_comm : forall ML M M', app_subst' ML (fst' M) M' -> exists M1', M' = fst' M1' /\ app_subst' ML M M1'. Theorem app_subst'_snd_comm : forall ML M M', app_subst' ML (snd' M) M' -> exists M1', M' = snd' M1' /\ app_subst' ML M M1'. Theorem app_subst'_abs_comm : forall ML R M', app_subst' ML (abs' R) M' -> exists R', M' = abs' R' /\ nabla x, app_subst' ML (R x) (R' x). Theorem app_subst'_unit_comm : forall ML M', app_subst' ML unit' M' -> M' = unit'. Theorem app_subst'_app_comm : forall ML M1 M2 M', app_subst' ML (app' M1 M2) M' -> exists M1' M2', M' = app' M1' M2' /\ app_subst' ML M1 M1' /\ app_subst' ML M2 M2'. Theorem app_subst'_meta_app_comm : forall ML R M M1, app_subst' ML (R M) M1 -> exists R' M', M1 = R' M' /\ (nabla (x:tm'), app_subst' ML (R x) (R' x)) /\ app_subst' ML M M'.induction on 1. intros. case H1. exists R. exists M. search. apply IH to H2 with R = (R V), M = (M V). exists R'. exists M'. search.Theorem app_subst'_meta_app_abs_comm : forall ML R M M1, app_subst' ML (R M) M1 -> exists R' M', M1 = R' M' /\ (nabla (x:tm' -> tm'), app_subst' ML (R x) (R' x)) /\ (nabla y, app_subst' ML (M y) (M' y)).induction on 1. intros. case H1. exists R. exists M. search. apply IH to H2 with R = (R V), M = (M V). exists R'. exists M'. search.Theorem app_subst'_hbase_comm : forall ML M P, app_subst' ML (hbase M) P -> exists M', P = hbase M' /\ app_subst' ML M M'. Theorem app_subst'_habs_comm : forall ML R P, app_subst' ML (habs R) P -> exists R', P = habs R' /\ nabla x, app_subst' ML (R x) (R' x). Theorem app_subst'_htm_comm : forall ML FE FE' M M', app_subst' ML (htm FE M) (htm FE' M') -> app_subst'_list ML FE FE' /\ app_subst' ML M M'. Theorem app_subst'_list_nil_comm : forall ML M, app_subst'_list ML cnil M -> M = cnil. Theorem app_subst'_list_comm : forall ML X L M, app_subst'_list ML (ccons X L) M -> exists X' L', M = ccons X' L' /\ app_subst' ML X X' /\ app_subst'_list ML L L'. Theorem app_subst'_list_comm1 : forall ML X L M, is_tm'_list M -> app_subst'_list ML M (ccons X L) -> exists X' L', M = ccons X' L' /\ app_subst' ML X' X /\ app_subst'_list ML L' L.induction on 2. intros. case H2. search. apply is_tm'_list_inst to H1 with V = V. apply IH to _ H3. case H1. case H5. case H5. search.% Composition lemmas for applications of substitutions Theorem app_subst'_pair_compose : forall ML M1 M2 M1' M2', app_subst' ML M1 M1' -> app_subst' ML M2 M2' -> app_subst' ML (pair' M1 M2) (pair' M1' M2'). Theorem app_subst'_abs_compose : forall ML R R', nabla x, app_subst' ML (R x) (R' x) -> app_subst' ML (abs' R) (abs' R'). Theorem app_subst'_let_compose : forall ML M1 M2 M1' M2', nabla x, app_subst' ML M1 M1' -> app_subst' ML (M2 x) (M2' x) -> app_subst' ML (let' M1 M2) (let' M1' M2'). Theorem app_subst'_hbase_compose : forall ML M M', app_subst' ML M M' -> app_subst' ML (hbase M) (hbase M'). Theorem app_subst'_habs_compose : forall ML R R', nabla x, app_subst' ML (R x) (R' x) -> app_subst' ML (habs R) (habs R'). Theorem app_subst'_htm_compose : forall ML L L' M M', app_subst'_list ML L L' -> app_subst' ML M M' -> app_subst' ML (htm L M) (htm L' M'). Theorem app_subst'_list_compose : forall ML X X' L L', app_subst' ML X X' -> app_subst'_list ML L L' -> app_subst'_list ML (ccons X L) (ccons X' L'). Theorem app_subst'_list_nil : forall ML, subst' ML -> app_subst'_list ML cnil cnil. Theorem app_subst'_list_nil1 : forall ML L, is_tm'_list L -> app_subst'_list ML L cnil -> L = cnil.induction on 2. intros. case H2. search. case H1. search. apply is_tm'_list_inst to H4 with V = V. apply IH to _ H3.Theorem app_subst'_list_prune : forall ML M M', nabla (x:tm'), app_subst'_list ML M (M' x) -> exists M'', M' = y\M''.