Click on a command or tactic to see a detailed view of its use.

Specification "trans".

Import "typing". [View typing]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% Source language substitutions %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Substitutions
Define subst : list (map tm tm) -> prop by
  subst nil;
  nabla x, subst (map x V :: ML) :=
    subst ML /\ {val V} /\ {tm V}.

Define vars_of_subst : list (map tm tm) -> list tm -> prop by
  vars_of_subst nil nil;
  nabla x, vars_of_subst (map x V :: ML) (x :: L) :=
    vars_of_subst ML L.

% Lemmas about substitutions
Theorem subst_mem : forall ML E,
  subst ML -> member E ML -> exists X V,
    E = map X V /\ name X /\ {val V} /\ {tm V}.
induction on 1. intros. case H1.
  case H2.
  case H2. search. backchain IH.
Theorem subst_extend : forall ML V, nabla x,
  subst ML -> {tm V} -> {val V} -> subst (map x V :: ML).
intros. unfold. search. search. search.
% Lemmas of substitutions
Theorem app_subst_exists: forall ML (M:tm),
  subst ML -> exists M', app_subst ML M M'.
induction on 1. intros. case H1.
  search.
  apply IH to H2 with M = M V. search.
Theorem subst_closed_tm_eq : forall M (ML:list (map tm tm)) M',
  {tm M} -> app_subst ML M M' -> M = M'.
induction on 2. intros. case H2.
  search.
  apply sclosed_tm_prune to H1. apply IH to _ H3. search.
Theorem subst_inst : forall (ML:list (map tm tm)) (M:tm -> tm) 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 sclosed_tm_prune to H1. unfold. intros. apply IH to H1 H3. search.
Theorem explct_meta_subst_comm : forall ML (M:tm -> tm) E V, nabla n,
  {tm V} -> app_subst ML (M n) (E n) -> app_subst (map n V :: ML) (M n) (E V).
intros. unfold. intros. 
  backchain subst_inst with M = M, M' = E, x = n1.
Theorem subst_closed_tm : forall M ML,
  {tm M} -> subst ML -> app_subst ML M M.
induction on 2. intros. case H2.
  search.
  apply sclosed_tm_prune to H1. apply IH to H1 H3. search.
Theorem subst_var : forall V ML X,
  subst ML -> member (map X V) ML -> app_subst ML X V.
induction on 2. intros. case H2.
  case H1. unfold. backchain subst_closed_tm.
  case H1. apply member_prune to H3. unfold. backchain IH.
Theorem subst_var_eq : forall V ML E X,
  subst ML -> member (map X V) ML -> app_subst ML X E -> E = V.
intros. apply subst_var to H1 H2. apply app_subst_det to H3 H4. search.
Theorem subst_nabla : forall ML, nabla (x:tm),
  subst ML -> app_subst ML x x.
induction on 1. intros. case H1.
  search.
  unfold. backchain IH.
  
Theorem subst_result_closed_tm : forall ML L M M' Vs,
  tm_sctx L -> {L |- tm M} -> vars_of_tm_sctx 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 T M M' Vs,
  {is_sty T} -> sctx L -> {L |- of M T} -> vars_of_sctx L Vs ->
  subst ML -> vars_of_subst ML Vs -> app_subst 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 subst_result_closed_tm.
% Commutative property of applications of substitions
Theorem app_subst_pred_comm : forall (ML:list (map tm tm)) M M',
  app_subst ML (pred M) M' -> exists M'', M' = pred M'' /\ app_subst ML M M''.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst_ifz_comm : forall (ML:list (map tm tm)) 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'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst_let_comm : forall (ML:list (map tm tm)) 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).
 
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst_fix_comm : forall (ML:list (map tm tm)) 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).
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst_app_comm : forall (ML:list (map tm tm)) 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'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst_plus_comm : forall (ML:list (map tm tm)) 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'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst_pair_comm : forall (ML:list (map tm tm)) 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'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst_fst_comm : forall (ML:list (map tm tm)) M M',
  app_subst ML (fst M) M' -> exists M1',  M' = fst M1' /\
    app_subst ML M M1'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst_snd_comm : forall (ML:list (map tm tm)) M M',
  app_subst ML (snd M) M' -> exists M1',  M' = snd M1' /\
    app_subst ML M M1'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst_meta_app_comm : 
  forall (ML:list (map tm tm)) (R:tm -> tm) (M:tm) P,
  app_subst ML (R M) P -> exists R' M', P = R' M' /\
    app_subst ML M M' /\ nabla x, app_subst 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_subst_pred_compose : forall (ML:list (map tm tm)) M M',
  app_subst ML M M' -> app_subst ML (pred M) (pred M').
induction on 1. intros. case H1.
  search.
  unfold. backchain IH.
Theorem app_subst_ifz_compose : forall (ML:list (map tm tm)) M1 M2 M1' M2' M3 M3',
  app_subst ML M1 M1' -> app_subst ML M2 M2' -> app_subst ML M3 M3' ->
    app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3').
induction on 1. intros. case H1.
  case H2. case H3. search.
  case H2. case H3. unfold. backchain IH.
Theorem app_subst_plus_compose : forall (ML:list (map tm tm)) M1 M2 M1' M2',
  app_subst ML M1 M1' -> app_subst ML M2 M2' -> app_subst ML (plus M1 M2) (plus M1' M2').
induction on 1. intros. case H1.
  case H2. search.
  case H2. unfold. backchain IH.
Theorem app_subst_fst_compose : forall (ML:list (map tm tm)) M M',
  app_subst ML M M' -> app_subst ML (fst M) (fst M').
induction on 1. intros. case H1.
  search.
  unfold. backchain IH.
Theorem app_subst_snd_compose : forall (ML:list (map tm tm)) M M',
  app_subst ML M M' -> app_subst ML (snd M) (snd M').
induction on 1. intros. case H1.
  search.
  unfold. backchain IH.
Theorem app_subst_pair_compose : forall (ML:list (map tm tm)) M1 M2 M1' M2',
  app_subst ML M1 M1' -> app_subst ML M2 M2' -> app_subst ML (pair M1 M2) (pair M1' M2').
induction on 1. intros. case H1.
  case H2. search.
  case H2. unfold. backchain IH.
Theorem app_subst_app_compose : forall (ML:list (map tm tm)) M1 M2 M1' M2',
  app_subst ML M1 M1' -> app_subst ML M2 M2' -> app_subst ML (app M1 M2) (app M1' M2').
induction on 1. intros. case H1.
  case H2. search.
  case H2. unfold. backchain IH.
Theorem app_subst_fix_compose : forall (ML:list (map tm tm)) M M', nabla f x,
  app_subst ML (M f x) (M' f x) -> app_subst 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_subst_let_compose : forall (ML:list (map tm tm)) 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').
induction on 1. intros. case H1.
  case H2. search.
  case H2. unfold. backchain IH with x = n1.

%
Define vars_in_subst : list tm -> list (map tm tm) -> prop by
  vars_in_subst nil ML;
  vars_in_subst (X :: Vs) ML :=
    vars_in_subst Vs ML /\ exists V, member (map X V) ML.

Theorem vars_in_subst_extend : forall Vs L E,
  vars_in_subst Vs L -> vars_in_subst Vs (E :: L).
induction on 1. intros. case H1.
  search.
  apply IH to H2 with E = E. search.
Theorem subst_var_rsl_clear : forall ML V (M: tm -> tm) M', nabla x,
  subst (ML x) -> member (map 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 H8. apply IH to H6 H4 H5. search.
    % The head of (ML x) is x
    search.
Theorem subst_var_inst : forall ML V (M: tm -> tm) M', nabla x,
  subst (ML x) -> member (map x V) (ML x) -> app_subst (ML x) (M x) M' ->
    app_subst (ML x) (M V) M'.
induction on 2. intros. case H2.
  % The head of (ML x) is x
  case H3. search.
  % The head of (ML x) is not x
  case H3. 
    case H1.
      apply closed_tm_prune to H8.
      apply subst_mem to H6 H4. apply closed_tm_prune to H11.
      unfold. apply IH to H6 H4 H5. search.
    apply member_prune to H4.
Theorem subst_result_closed_tm_alt : 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.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% Target language substitutions  %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Explicit target substitutions 
Define subst' : list (map tm' tm') -> prop by
  subst' nil;
  nabla x, subst' (map x V :: ML) :=
    subst' ML /\ {val' V} /\ {tm' V}.

Define vars_of_subst' : list (map tm' tm') -> list tm' -> prop by
  vars_of_subst' nil nil;
  nabla x, vars_of_subst' (map x V :: ML) (x :: L) :=
    vars_of_subst' ML L.

Theorem app_subst'_exists: forall ML (M:tm'),
  subst' ML -> exists M', app_subst ML M M'.
induction on 1. intros. case H1.
  search.
  apply IH to H2 with M = M V. search.
% Lemmas about substitutions
Theorem subst'_nabla : forall ML, nabla (x:tm'),
  subst' ML -> app_subst ML x x.
induction on 1. intros. case H1.
  search.
  unfold. backchain IH.
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 subst'_mem : forall ML E,
  subst' ML -> member E ML -> exists X V,
    E = map X V /\ name X /\ {val' V} /\ {tm' V}.
induction on 1. intros. case H1.
  case H2.
  case H2. search. backchain IH.
Theorem subst'_extend : forall ML V, nabla x,
  subst' ML -> {tm' V} -> {val' V} -> subst' (map x V :: ML).
intros. unfold. search. search. search.
 
Theorem subst'_closed_tm_eq : forall M (ML:list (map tm' tm')) M',
  {tm' M} -> app_subst ML M M' -> M = M'.
induction on 2. intros. case H2.
  search.
  apply closed_tm'_prune to H1. apply IH to _ H3. search.
Theorem subst'_closed_tm : forall M ML,
  {tm' M} -> subst' ML -> app_subst ML M M.
induction on 2. intros. case H2.
  search.
  apply closed_tm'_prune to H1. apply IH to H1 H3. search.
Theorem subst'_var : forall V ML X,
  subst' ML -> member (map 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 member_prune to H3. unfold. intros. backchain IH.
Theorem subst'_var_eq : forall V ML E X,
  subst' ML -> member (map X V) ML -> app_subst ML X E -> E = V.
intros. apply subst'_var to H1 H2. apply app_subst_det to H3 H4. search.
Theorem subst'_inst : 
  forall (ML:list (map tm' tm')) (M:tm' -> tm') 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:tm' -> tm') E V, nabla n,
  {tm' V} -> app_subst ML (M n) (E n) -> app_subst (map n V :: ML) (M n) (E V).
intros. unfold. intros. 
  backchain subst'_inst with M = M, M' = E, x = n1.

%% lemmas for hoisted terms
Theorem subst'_closed_tm''_eq : forall M (ML:list (map tm' tm')) M',
  {tm'' M} -> app_subst ML M M' -> M = M'.
induction on 2. intros. case H2.
  search.
  apply closed_tm''_prune to H1. apply IH to _ H3. search.
Theorem subst'_closed_tm''_body_eq : forall M (ML:list (map tm' tm')) 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:list (map tm' tm')) M M',
  app_subst ML (pred' M) M' -> exists M'', M' = pred' M'' /\ app_subst ML M M''.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_ifz_comm : forall (ML:list (map tm' tm')) 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'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_let_comm : forall (ML:list (map tm' tm')) 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).
 
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_clos_comm : forall (ML:list (map tm' tm')) 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'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_open_comm : forall (ML:list (map tm' tm')) 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'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_plus_comm : forall (ML:list (map tm' tm')) 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'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_pair_comm : forall (ML:list (map tm' tm')) 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'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_fst_comm : forall (ML:list (map tm' tm')) M M',
  app_subst ML (fst' M) M' -> exists M1',  M' = fst' M1' /\
    app_subst ML M M1'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_snd_comm : forall (ML:list (map tm' tm')) M M',
  app_subst ML (snd' M) M' -> exists M1',  M' = snd' M1' /\
    app_subst ML M M1'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_abs_comm : forall (ML:list (map tm' tm')) R M',
  app_subst ML (abs' R) M' -> 
    exists R', M' = abs' R' /\ nabla x, app_subst ML (R x) (R' x).
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_unit_comm : forall (ML:list (map tm' tm')) M',
  app_subst ML unit' M' -> M' = unit'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_app_comm : forall (ML:list (map tm' tm')) 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'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_meta_app_comm : forall (ML:list (map tm' tm')) (R:tm' -> tm') 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:list (map tm' tm')) (R:(tm' -> tm') -> tm') 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:list (map tm' tm')) M P,
  app_subst ML (hbase M) P -> exists M', 
    P = hbase M' /\ app_subst ML M M'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_habs_comm : forall (ML:list (map tm' tm')) R P,
  app_subst ML (habs R) P -> exists R',
    P = habs R' /\ nabla x, app_subst ML (R x) (R' x).
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_htm_comm : forall (ML:list (map tm' tm')) FE FE' M M',
  app_subst ML (htm FE M) (htm FE' M') ->
    app_subst_list ML FE FE' /\ app_subst ML M M'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.

% Composition lemmas for applications of substitutions
Theorem app_subst'_pair_compose : forall (ML:list (map tm' tm')) M1 M2 M1' M2',
  app_subst ML M1 M1' -> app_subst ML M2 M2' -> app_subst ML (pair' M1 M2) (pair' M1' M2').
induction on 1. intros. case H1.
  case H2. search.
  case H2. unfold. backchain IH.
Theorem app_subst'_abs_compose : forall (ML:list (map tm' tm')) R R',
  nabla x, app_subst ML (R x) (R' x) -> app_subst ML (abs' R) (abs' R').
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_let_compose : forall (ML:list (map tm' tm')) 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').
induction on 1. intros. case H1.
  case H2. search.
  case H2. unfold. backchain IH with x = n1.
Theorem app_subst'_hbase_compose : forall (ML:list (map tm' tm')) M M',
  app_subst ML M M' -> app_subst ML (hbase M) (hbase M').
induction on 1. intros. case H1.
  search.
  unfold. apply IH to H2. search.
Theorem app_subst'_habs_compose : forall (ML:list (map tm' tm')) R R', nabla x,
  app_subst ML (R x) (R' x) -> app_subst ML (habs R) (habs R').
induction on 1. intros. case H1.
  search.
  unfold. apply IH to H2. search.
Theorem app_subst'_htm_compose : forall (ML:list (map tm' tm')) L L' M M',
  app_subst_list ML L L' -> app_subst ML M M' ->
    app_subst ML (htm L M) (htm L' M').
induction on 1. intros. case H1.
  case H2. search.
  case H2. apply IH to H3 H4. search.

Theorem app_subst'_list_nil1 : forall (ML:list (map tm' tm')),
  subst' ML -> app_subst_list ML (nil:list tm') nil.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem app_subst'_list_nil2 : forall (ML:list (map tm' tm')) (L:list tm'), 
  is_list L -> app_subst_list ML L nil -> L = nil.
induction on 2. intros. case H2.
  search.
  case H1. search. 
    apply is_list_inst to H4 with V = V. apply IH to _ H3.