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

Specification "trans".

Import "util". [View util]

Close nat, ty, tm, tm', list tm, list tm', map tm tm', list (map tm tm').

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Source typing context with unique type assignments %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Typing context
Define sctx : olist -> prop by
  sctx nil;
  nabla x, sctx (of x T :: L) := sctx L /\ {is_sty T}.

Define vars_of_sctx : olist -> list tm -> prop by
  vars_of_sctx nil nil;
  nabla x, vars_of_sctx (of x T :: L) (x :: L') :=
    vars_of_sctx L L'.

% Lemmas of Typing
Theorem sctx_mem : forall SL O,
  sctx SL -> member O SL -> exists X T, O = of X T /\ name X /\ {is_sty T}.
induction on 2. intros. case H2.
  case H1. search.
  case H1. backchain IH.
Theorem sctx_var_mem : forall L T M,
  sctx L -> {L |- of M T} -> name M -> member (of M T) L.
intros. case H3. case H2.
  apply sctx_mem to H1 H5. case H4. search.
Theorem sof_nat_inv : forall L N T,
  sctx L -> {L |- of (nat N) T} -> T = tnat.
intros. case H2. search.
  apply sctx_mem to _ H4. case H3. case H5.
Theorem sof_pair_inv : forall L M1 M2 T,
  sctx L -> {L |- of (pair M1 M2) T} -> exists T1 T2, T = prod T1 T2.
intros. case H2. search.
  apply sctx_mem to _ H4. case H3. case H5.
Theorem sof_unit_inv : forall L T,
  sctx L -> {L |- of unit T} -> T = tunit.
intros. case H2. search.
  apply sctx_mem to _ H4. case H3. case H5.
Theorem sctx_focus_inv : forall L D G,
  sctx L -> member D L -> {L, [D] |- G} -> exists A T, G = of A T /\ name A.
intros. apply sctx_mem to H1 H2. case H3. search.
Theorem s_is_sty_str : forall L T,
  sctx L -> {L |- is_sty T} -> {is_sty T}.
 
induction on 2. intros. case H2.
  search.
  search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply sctx_mem to H1 H4. case H3.
Theorem sof_is_sty : forall L M T,
  sctx L -> {L |- of M T} -> {is_sty T}.
induction on 2. intros. case H2.
  search.
  search.
  search.
  backchain IH with M = M1.
  search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. case H4. search.
  apply IH to _ H3. case H4. search.
  apply IH to _ H3. backchain IH with 
    L = (of n1 T1 :: L), M = (R n1). 
  backchain s_is_sty_str with L = L.
  apply IH to _ H3. case H5. search.
  apply sctx_mem to H1 H4. case H3. search.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Properties about well-formed terms in the source lanugage (with duplications) %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Term context
Define tm_sctx : olist -> prop by
  tm_sctx nil;
  nabla x, tm_sctx (tm x :: L) := tm_sctx L.

Define vars_of_tm_sctx : olist -> list tm -> prop by
  vars_of_tm_sctx nil nil;
  nabla x, vars_of_tm_sctx (tm x :: L) (x :: L') :=
    vars_of_tm_sctx L L'.

Theorem tm_sctx_mem : forall E L,
  tm_sctx L -> member E L -> exists X, E = tm X /\ name X.
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to _ H3. search.
Theorem sctx_to_tm_sctx : forall L Vs,
  sctx L -> vars_of_sctx L Vs -> 
    exists SL, tm_sctx SL /\ vars_of_tm_sctx SL Vs.
induction on 2. intros. case H2.
  search.
  case H1. apply IH to _ H3. search.
Theorem sctx_tm_sctx_sync : forall L Vs SL M T,
  vars_of_sctx L Vs -> vars_of_tm_sctx SL Vs -> member (of M T) L -> 
    member (tm M) SL.
induction on 3. intros. case H3.
  case H1. case H2. search.
  case H1. case H2. unfold. backchain IH.
Theorem sclosed_tm_prune_aux : forall M L, nabla (x:tm),
  tm_sctx L -> {L |- tm (M x)} -> exists M', M = y\ M'.
induction on 2. intros. case H2.
  search.
  apply IH to _ H3. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. apply IH to _ H4. apply IH to _ H5. search.
  search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. search.
  apply IH to _ H3. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply tm_sctx_mem to H1 H4. case H3. apply member_prune to H4. search.
Theorem sclosed_tm_prune : forall M, nabla (x:tm),
  {tm (M x)} -> exists M', M = y\ M'.
intros. apply sclosed_tm_prune_aux to _ H1. search.
Theorem sof_to_tm : forall L Vs SL M T,
  {is_sty T} -> sctx L -> vars_of_sctx L Vs -> tm_sctx SL -> vars_of_tm_sctx SL Vs ->
    {L |- of M T} -> {SL |- tm M}.
induction on 6. intros. case H6.
  search.
  assert {SL |- tm M1}. backchain IH. search.
  assert {SL |- tm M1}. backchain IH. assert {SL |- tm M2}. backchain IH. search.
  assert {SL |- tm M1}. backchain IH. 
    assert {SL |- tm M2}. backchain IH. assert {SL |- tm M3}. backchain IH with T = tnat. search.
  search.
  case H1. assert {SL |- tm M1}. backchain IH with T = T1. 
    assert {SL |- tm M2}. backchain IH with T = T2. search.
  assert {SL |- tm M1}. backchain IH with T = prod T T2. 
    backchain sof_is_sty. search.
  assert {SL |- tm M1}. backchain IH with T = prod T1 T. 
    backchain sof_is_sty. search.
  apply sof_is_sty to _ H7. assert {SL |- tm M1}. backchain IH with T = T1. 
    assert {SL, tm n1 |- tm (R n1)}. 
      backchain IH with L = of n1 T1 :: L, T = T.
    search.
  apply s_is_sty_str to _ H8. case H9.
    assert {SL, tm n1, tm n2 |- tm (R n1 n2)}.
      backchain IH with L = of n2 T1 :: of n1 (arr T1 T2) :: L, T = T2.
    search.
  assert {SL |- tm M1}. backchain IH with T = arr T1 T. backchain sof_is_sty. 
    assert {SL |- tm M2}. backchain IH with T = T1. backchain sof_is_sty. search.
  apply sctx_mem to _ H8. case H7. 
    assert member (tm M) SL. backchain sctx_tm_sctx_sync.
    search.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Source typing context with possibly duplicated type assignments %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Typing contexts
Define ctx : olist -> prop by
  ctx nil;
  ctx (of X T :: L) := ctx L /\ name X /\ {is_sty T} /\
         forall T', (member (of X T') L -> T = T').

% Accumulate the variables in the source context
Define vars_of_ctx : olist -> list tm -> prop by
  vars_of_ctx nil nil;
  vars_of_ctx (of X T :: L) (X :: Vs) := vars_of_ctx L Vs.

Theorem ctx_islist : forall L,
  ctx L -> is_list L.
induction on 1. intros. case H1.
  search.
  unfold. backchain IH.
Theorem ctx_mem : forall SL O,
  ctx SL -> member O SL -> exists X T, O = of X T /\ name X /\ {is_sty T}.
induction on 1. intros. case H1.
  case H2.
  case H2. search. backchain IH.
Theorem ctx_mem_sync : forall L X T T',
  ctx L -> member (of X T) L -> member (of X T') L -> T = T'.
induction on 2. intros. case H2.
  case H3.
    search.
    case H1. backchain H8.
  case H3.
    case H1. apply H8 to H4. search.
    case H1. backchain IH.
Theorem ctx_extend : forall L T, nabla x, 
  ctx L -> {is_sty T} -> ctx (of x T :: L).
intros. unfold. search. search. search.
  intros. apply member_prune to H3.
Theorem is_sty_str : forall L T,
  ctx L -> {L |- is_sty T} -> {is_sty T}.
 
induction on 2. intros. case H2.
  search.
  search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply ctx_mem to H1 H4. case H3.
Theorem of_is_sty : forall L M T,
  ctx L -> {L |- of M T} -> {is_sty T}.
induction on 2. intros. case H2.
  search.
  search.
  search.
  backchain IH with M = M1.
  search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. case H4. search.
  apply IH to _ H3. case H4. search.
  apply IH to _ H3. backchain IH with 
    L = (of n1 T1 :: L), M = (R n1). backchain ctx_extend.
  backchain is_sty_str with L = L.
  apply IH to _ H3. case H5. search.
  apply ctx_mem to H1 H4. case H3. search.
Theorem sty_to_cty : forall T,
  {is_sty T} -> {is_cty T}.
induction on 1. intros. case H1.
  search.
  search.
  apply IH to H2. apply IH to H3. search.
  apply IH to H2. apply IH to H3. search.
Theorem ctx_name : forall L Vs X,
  ctx L -> vars_of_ctx L Vs -> {memb X Vs} -> name X.
induction on 3. intros. case H3.
  case H2. case H1. search.
  case H2. case H1. apply IH to _ _ H4. search.
Theorem ctx_subset : forall L L',
  ctx L -> subset L' L -> ctx L'.
induction on 2. intros. case H2.
  search.
  apply ctx_mem to _ H3. unfold.
    backchain IH.
    search.
    search.
    intros. apply subset_mem_trans to H4 H7. apply ctx_mem_sync to _ H3 H8. search.
  
% Lemmas of typing
Theorem of_nat_inv : forall L N T,
  ctx L -> {L |- of (nat N) T} -> T = tnat.
intros. case H2. search.
  apply ctx_mem to _ H4. case H3. case H5.
Theorem of_var_inv : forall M L T,
  ctx L -> {L |- of M T} -> name M -> member (of M T) L.
intros. case H3. case H2. apply ctx_mem to _ H5. case H4. search.
Theorem of_weakening : forall L L' M T,
  ctx L -> subset L L' -> {L |- of M T} -> {L' |- of M T}.
induction on 3. intros. case H3.
  search.
  apply IH to _ _ H4. search.
  apply IH to _ _ H4. apply IH to _ _ H5. search.
  apply IH to _ _ H4. apply IH to _ _ H5. apply IH to _ _ H6. search.
  search.
  apply IH to _ _ H4. apply IH to _ _ H5. search.
  apply IH to _ _ H4. search.
  apply IH to _ _ H4. search.
  apply IH to _ _ H4. apply IH to _ _ H5 with L' = (of n1 T1 :: L'). 
    backchain subset_extend. backchain ctx_extend. backchain of_is_sty. search.
  apply is_sty_str to _ H5.
  apply IH to _ _ H4 with L' = (of n2 T1 :: of n1 (arr T1 T2) :: L'). 
    backchain subset_extend. backchain subset_extend. 
    backchain ctx_extend. backchain ctx_extend. case H6. search.
    search.
  apply IH to _ _ H4. apply IH to _ _ H5. search.
  apply ctx_mem to _ H5. case H4. 
    assert member (of M T) L'. backchain subset_mem_trans. search.
Theorem ctx_focus_inv : forall L D G,
  ctx L -> member D L -> {L, [D] |- G} -> exists A T, G = of A T /\ name A.
intros. apply ctx_mem to H1 H2. case H3. search.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Properties about well-formed terms in the source lanugage (with duplications) %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Well-formed term contexts
Define tm_ctx : olist -> prop by
  tm_ctx nil;
  tm_ctx (tm X :: L) := tm_ctx L /\ name X.

Define vars_of_tm_ctx : olist -> list tm -> prop by
  vars_of_tm_ctx nil nil;
  vars_of_tm_ctx (tm X :: L) (X :: L') :=
    vars_of_tm_ctx L L'.

Theorem tm_ctx_mem : forall E L,
  tm_ctx L -> member E L -> exists X, E = tm X /\ name X.
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to _ H3. search.
Theorem ctx_mem_to_lst_mem : forall L Vs X T,
  vars_of_ctx L Vs -> member (of X T) L -> {memb X Vs}.
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to  H4 H3. search.
Theorem lst_mem_to_ctx_mem : forall L Vs X,
  vars_of_ctx L Vs -> {memb X Vs} -> 
    exists T, member (of X T) L.
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to H4 H3. search.
Theorem ctx_to_tm_ctx : forall L Vs,
  ctx L -> vars_of_ctx L Vs -> 
    exists SL, tm_ctx SL /\ vars_of_tm_ctx SL Vs.
induction on 2. intros. case H2.
  search.
  case H1. apply IH to _ H3. search.
Theorem ctx_tm_ctx_sync : forall L Vs SL M T,
  vars_of_ctx L Vs -> vars_of_tm_ctx SL Vs -> member (of M T) L -> 
    member (tm M) SL.
induction on 3. intros. case H3.
  case H1. case H2. search.
  case H1. case H2. unfold. backchain IH.
Theorem tm_cut : forall L M V, nabla x,
  {tm V} -> tm_ctx (L x) -> {L x, tm x |- tm (M x)} ->  {L x |- tm (M V)}.
induction on 3. intros. case H3.
  search.
  apply IH to _ _ H4. search.
  apply IH to _ _ H4. apply IH to _ _ H5. search.
  apply IH to _ _ H4. apply IH to _ _ H5. apply IH to _ _ H6. search.
  search.
  apply IH to _ _ H4. apply IH to _ _ H5. search.
  apply IH to _ _ H4. search. 
  apply IH to _ _ H4. search.
  apply IH to _ _ H4. apply IH to _ _ H5 with x = n1. search.
  apply IH to _ _ H4 with x = n1. search.
  apply IH to _ _ H4. apply IH to _ _ H5. search.  
  case H5. case H4. search.
    apply tm_ctx_mem to H2 H6. case H7.
      case H4. search.
      case H4. search.
% closed terms do not contain nominal constants
Theorem closed_tm_prune_aux : forall M L, nabla (x:tm),
  tm_ctx L -> {L |- tm (M x)} -> exists M', M = y\ M'.
induction on 2. intros. case H2.
  search.
  apply IH to _ H3. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. apply IH to _ H4. apply IH to _ H5. search.
  search.   
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. search.
  apply IH to _ H3. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. apply IH to _ H3. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply tm_ctx_mem to H1 H4. case H3. apply member_prune to H4. search.
Theorem closed_tm_prune : forall M, nabla (x:tm),
  {tm (M x)} -> exists M', M = y\ M'.
intros. apply closed_tm_prune_aux to _ H1. search.
Theorem of_to_tm : forall L Vs SL M T,
  ctx L -> vars_of_ctx L Vs -> tm_ctx SL -> vars_of_tm_ctx SL Vs ->
    {L |- of M T} -> {SL |- tm M}.
induction on 5. intros. case H5.
  search.
  assert {SL |- tm M1}. backchain IH. search.
  assert {SL |- tm M1}. backchain IH. assert {SL |- tm M2}. backchain IH. search.
  assert {SL |- tm M1}. backchain IH. 
    assert {SL |- tm M2}. backchain IH. assert {SL |- tm M3}. backchain IH. search.
  search.
  assert {SL |- tm M1}. backchain IH. assert {SL |- tm M2}. backchain IH. search.
  assert {SL |- tm M1}. backchain IH. search.
  assert {SL |- tm M1}. backchain IH. search.
  assert {SL |- tm M1}. backchain IH. 
    assert {SL, tm n1 |- tm (R n1)}. 
      backchain IH with L = of n1 T1 :: L.
      backchain ctx_extend. backchain of_is_sty. 
    search.
  apply is_sty_str to _ H7.
    assert {SL, tm n1, tm n2 |- tm (R n1 n2)}.
      backchain IH with L = of n2 T1 :: of n1 (arr T1 T2) :: L.
      backchain ctx_extend. backchain ctx_extend. case H8. search.
    search.
  assert {SL |- tm M1}. backchain IH. assert {SL |- tm M2}. backchain IH. search.
  apply ctx_mem to _ H7. case H6. 
    assert member (tm M) SL. backchain ctx_tm_ctx_sync.
    search.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Target typing context with unique type assignments %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Typing contexts
Define ctx' : olist -> prop by
  ctx' nil;
  nabla x, ctx' (of' x T :: L) := ctx' L /\ {is_cty T}.

Define vars_of_ctx' : olist -> list tm' -> prop by
  vars_of_ctx' nil nil;
  vars_of_ctx' (of' X T :: L) (X :: Vs) := vars_of_ctx' L Vs.

Theorem ctx'_islist : forall L,
  ctx' L -> is_list L.
induction on 1. intros. case H1.
  search.
  unfold. backchain IH.
Theorem ctx'_mem : forall E L,
  ctx' L -> member E L -> exists M T, E = of' M T /\ name M /\ {is_cty T}.
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to _ H3. search.
Theorem ctx'_var_mem : forall L T M,
  ctx' L -> {L |- of' M T} -> name M -> member (of' M T) L.
intros. case H3. case H2.
  apply ctx'_mem to H1 H5. case H4. search.
Theorem ctx'_mem_sync : forall L X T T',
  ctx' L -> member (of' X T) L -> member (of' X T') L -> T = T'.
induction on 2. intros. case H2.
  case H3.
    search.
    case H1. apply member_prune to H4.
  case H3.
    case H1. apply member_prune to H4.
    case H1. apply IH to _ H4 H5. search.
Theorem vars_of_ctx'_prune2 : forall L Vs, nabla (x:tm'),
  vars_of_ctx' L (Vs x) -> exists Vs', Vs = y\Vs'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
% Lemmas of typing
Theorem of'_nat_inv : forall L N T,
  ctx' L -> {L |- of' (nat' N) T} -> T = tnat.
intros. case H2. search.
  apply ctx'_mem to _ H4. case H3. case H5.
Theorem is_cty_str : forall L T,
  ctx' L -> {L |- is_cty T} -> {is_cty T}.
induction on 2. intros. case H2.
  search.
  search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply ctx'_mem to H1 H4. case H3.
Theorem of'_is_cty : forall L M T,
  ctx' L -> {L |- of' M T} -> {is_cty T}.
induction on 2. intros. case H2.
  search.
  search.
  search.
  backchain IH with M = M1.
  search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. case H4. search.
  apply IH to _ H3. case H4. search.
  apply IH to _ H3. apply IH to _ H4. search. 
  apply is_cty_str to _ H4. apply IH to _ H3. search.
  apply IH to _ H3. case H5. search.
  apply IH to _ H3. case H5. case H6. search.
  apply IH to _ H3. case H5. search.
  apply ctx'_mem to H1 H4. case H3. search.
Theorem of'_str: forall L M T1 T, nabla x,
  ctx' L -> {is_cty T1} -> {L, of' x T1 |- of' M T} -> {L |- of' M T}.
induction on 3. intros. case H3.
  search.
  apply IH to _ _ H4. search.
  apply IH to _ _ H4. apply IH to _ _ H5. search.
  apply IH to _ _ H4. apply IH to _ _ H5. apply IH to _ _ H6. search.
  search.
  apply IH to _ _ H4. apply IH to _ _ H5. search.
  apply IH to _ _ H4. search.
  apply IH to _ _ H4. search.
  apply of'_is_cty to _ H4. apply IH to _ _ H4. apply IH to _ _ H5. search.
  apply is_cty_str to _ H5. apply IH to _ _ H4. search.
  apply IH to _ _ H4. apply IH to _ _ H5. search.
  apply IH to _ _ H4. apply IH to _ _ H5. search.
  apply IH to _ _ H4. apply IH to _ _ H5. search.
  apply ctx'_mem to _ H5. case H5.
    case H4.
    case H4. search.
Theorem of''_env_str: forall L FE T TE, nabla x,
  ctx' L -> {is_cty T} -> {L, of' x T |- of''_env FE TE} -> 
    {L |- of''_env FE TE}.
induction on 3. intros. case H3.
  search.
  apply of'_str to _ _ H4. apply IH to _ _ H5. search.
  apply ctx'_mem to _ H5. case H4.
Theorem ctx'_focus_inv : forall L D G,
  ctx' L -> member D L -> {L, [D] |- G} -> exists A T, G = of' A T /\ name A.
intros. apply ctx'_mem to H1 H2. case H3. search.
Theorem of''_env_is_cty : forall L FE TE,
  ctx' L -> {L |- of''_env FE TE} -> {is_cty TE}.
induction on 2. intros. case H2.
  search.
  apply of'_is_cty to _ H3. apply IH to _ H4. search.
  apply ctx'_mem to _ H4. case H3.
Theorem of''_env_tm'_list : forall L FE1 TE,
  ctx' L -> {L |- of''_env FE1 TE} -> is_list FE1.
induction on 2. intros. case H2.
  search.
  apply IH to _ H4. search.
  apply ctx'_focus_inv to _ _ H3.
Theorem of''_body_is_cty : forall L TE M T,
  ctx' L -> {is_cty TE} -> {L |- of''_body TE M T} -> {is_cty T}.
induction on 3. intros. case H3.
  apply of'_is_cty to _ H4. search.
  case H2. apply IH to _ _ H4. search.
  apply ctx'_mem to _ H5. case H4.
Theorem of''_is_cty: forall L M T,
  ctx' L -> {L |- of'' M T} -> {is_cty T}.
induction on 2. intros. case H2.
  apply of'_is_cty to _ H3. search.
  apply of'_is_cty to _ H3. apply IH to _ H4. search.
  apply ctx'_focus_inv to _ _ H3.
Theorem of''_to_alter_ver : forall L FE M T,
  ctx' L -> {L |- of'' (htm FE M) T} -> exists TE,
    {L |- of''_env FE TE} /\ {L |- of''_body TE M T}.
induction on 2. intros. case H2.
  search.
  apply of'_is_cty to _ H3. apply IH to _ H4.
    apply of''_env_str to _ _ H6. search.
  apply ctx'_focus_inv to _ _ H3.
 
Theorem of''_from_alter_ver : forall L FE TE M T,
  ctx' L -> {L |- of''_env FE TE} -> {L |- of''_body TE M T} ->
  {L |- of'' (htm FE M) T}.
induction on 3. intros. case H3.
  case H2.
    search.
    apply ctx'_focus_inv to _ _ H5. 
  case H2.
    apply is_cty_str to _ H5. apply IH to _ H7 H4. search.
    apply ctx'_focus_inv to _ _ H6. 
  apply ctx'_focus_inv to _ _ H4.
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Properties about well-formed terms in the target lanugage %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Define tm'_ctx : olist -> prop by
  tm'_ctx nil;
  nabla x, tm'_ctx (tm' x :: L) := tm'_ctx L.

Define vars_of_tm'_ctx : olist -> list tm' -> prop by
  vars_of_tm'_ctx nil nil;
  nabla x, vars_of_tm'_ctx (tm' x :: L) (x :: L') :=
    vars_of_tm'_ctx L L'.

Theorem vars_of_tm'_ctx_prune1 : forall L Vs, nabla (x:tm'),
  vars_of_tm'_ctx (L x) Vs -> exists L', L = y\L'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
Theorem tm'_ctx_mem : forall E L,
  tm'_ctx L -> member E L -> exists X, E = tm' X /\ name X.
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to _ H3. search.
Theorem ctx'_to_tm'_ctx : forall L Vs,
  ctx' L -> vars_of_ctx' L Vs -> 
    exists SL, tm'_ctx SL /\ vars_of_tm'_ctx SL Vs.
induction on 2. intros. case H2.
  search.
  case H1. apply IH to _ H3. 
    apply vars_of_ctx'_prune2 to H3. 
    apply vars_of_tm'_ctx_prune1 to H7. search.
Theorem ctx'_tm'_ctx_sync : forall L Vs SL M T,
  vars_of_ctx' L Vs -> vars_of_tm'_ctx SL Vs -> member (of' M T) L -> 
    member (tm' M) SL.
induction on 3. intros. case H3.
  case H1. case H2. search.
  case H1. case H2. unfold. backchain IH.
% closed terms do not contain nominal constants
Theorem closed_tm'_prune_aux : forall M L, nabla (x:tm'),
  tm'_ctx L -> {L |- tm' (M x)} -> exists M', M = y\ M'.
induction on 2. intros. case H2.
  search.
  apply IH to _ H3. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. apply IH to _ H4. apply IH to _ H5. search.
  search.   
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. search.
  apply IH to _ H3. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. apply IH to _ H3. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply IH to _ H3. apply IH to _ H4. search.
  apply tm'_ctx_mem to H1 H4. case H3. apply member_prune to H4. search.
Theorem closed_tm'_prune : forall M, nabla (x:tm'),
  {tm' (M x)} -> exists M', M = y\ M'.
intros. apply closed_tm'_prune_aux to _ H1. search.
Theorem of'_to_tm' : forall L Vs CL M T,
  ctx' L -> vars_of_ctx' L Vs -> tm'_ctx CL -> vars_of_tm'_ctx CL Vs ->
    {L |- of' M T} -> {CL |- tm' M}.
induction on 5. intros. case H5.
  search.
  assert {CL |- tm' M1}. backchain IH. search.
  assert {CL |- tm' M1}. backchain IH. assert {CL |- tm' M2}. backchain IH. search.
  assert {CL |- tm' M1}. backchain IH. 
    assert {CL |- tm' M2}. backchain IH. assert {CL |- tm' M3}. backchain IH. search.
  search.
  assert {CL |- tm' M1}. backchain IH. assert {CL |- tm' M2}. backchain IH. search.
  assert {CL |- tm' M1}. backchain IH. search.
  assert {CL |- tm' M1}. backchain IH. search.
  assert {CL |- tm' M1}. backchain IH.
    apply of'_is_cty to _ H6.
    assert {CL, tm' n1 |- tm' (R n1)}. 
      backchain IH with L = of' n1 T1 :: L.
    search.
  assert {CL, tm' n1 |- tm' (R n1)}.
    apply is_cty_str to _ H7.
    backchain IH with L = of' n1 T1 :: L.
    search.
  assert {CL |- tm' M1}. backchain IH. assert {CL |- tm' M2}. backchain IH. search.
  assert {CL |- tm' F}. backchain IH. assert {CL |- tm' E}. backchain IH. search.
  assert {CL |- tm' M1}. backchain IH. assert {CL |- tm' M2}. backchain IH. search.
  apply ctx'_mem to _ H7. case H6. 
    assert member (tm' M) CL. backchain ctx'_tm'_ctx_sync.
    search.
Theorem of''_body_to_tm'' : forall L Vs CL M T TE,
  ctx' L -> vars_of_ctx' L Vs -> tm'_ctx CL -> vars_of_tm'_ctx CL Vs ->
    {L |- of''_body TE M T} -> {CL |- tm''_body M}.
induction on 5. intros. case H5.
  apply of'_to_tm' to _ _ _ _ H6. search.
  apply is_cty_str to _ H7. 
    apply IH to _ _ _ _ H6 with Vs = (n1 :: Vs). search.
  apply ctx'_focus_inv to _ _ H6.
Theorem of''_to_tm'' : forall L Vs CL M T FE,
  ctx' L -> vars_of_ctx' L Vs -> tm'_ctx CL -> vars_of_tm'_ctx CL Vs ->
    {L |- of'' (htm FE M) T} -> {CL |- tm'' (htm FE M)}.
induction on 5. intros. case H5.
  apply of'_to_tm' to _ _ _ _ H6. search.
  apply of'_to_tm' to _ _ _ _ H6.
    apply of'_is_cty to _ H6.
    apply IH to _ _ _ _ H7 with Vs = (n1 :: Vs). search.
  apply ctx'_focus_inv to _ _ H6.

% Closedness lemmas for hoisted terms
Theorem closed_tm''_prune_aux : forall M L, nabla (x:tm'),
  tm'_ctx L -> {L |- tm'' (M x)} -> exists M', M = y\ M'.
induction on 2. intros. case H2.
  apply closed_tm'_prune_aux to _ H3. search.
  apply closed_tm'_prune_aux to _ H3. apply IH to _ H4. search.
  apply tm'_ctx_mem to H1 H4. case H3.
Theorem closed_tm''_prune : forall M, nabla (x:tm'),
  {tm'' (M x)} -> exists M', M = y\ M'.
intros. apply closed_tm''_prune_aux to _ H1. search.
Theorem closed_tm''_body_prune_aux : forall M L, nabla (x:tm'),
  tm'_ctx L -> {L |- tm''_body (M x)} -> exists M', M = y\ M'.
induction on 2. intros. case H2.
  apply closed_tm'_prune_aux to _ H3. search.
  apply IH to _ H3. search.
  apply tm'_ctx_mem to H1 H4. case H3.
Theorem closed_tm''_body_prune : forall M, nabla (x:tm'),
  {tm''_body (M x)} -> exists M', M = y\ M'.
intros. apply closed_tm''_body_prune_aux to _ H1. search.