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', map, tm_list, tm'_list, map_list. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% 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 -> tm_list -> prop by vars_of_sctx nil snil; nabla x, vars_of_sctx (of x T :: L) (scons 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}. Theorem sctx_var_mem : forall L T M, sctx L -> {L |- of M T} -> name M -> member (of M T) L. Theorem sof_nat_inv : forall L N T, sctx L -> {L |- of (nat N) T} -> T = tnat. Theorem sof_pair_inv : forall L M1 M2 T, sctx L -> {L |- of (pair M1 M2) T} -> exists T1 T2, T = prod T1 T2. Theorem sof_unit_inv : forall L T, sctx L -> {L |- of unit T} -> T = tunit. 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. 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 -> tm_list -> prop by vars_of_tm_sctx nil snil; nabla x, vars_of_tm_sctx (tm x :: L) (scons 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. 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. 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. 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_tm to H4. search.Theorem sclosed_tm_prune : forall M, nabla (x:tm), {tm (M x)} -> exists M', M = y\ M'. 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 -> tm_list -> prop by vars_of_ctx nil snil; vars_of_ctx (of X T :: L) (scons X Vs) := vars_of_ctx L Vs. Theorem ctx_islist : forall L, ctx L -> is_list L. Theorem ctx_mem : forall SL O, ctx SL -> member O SL -> exists X T, O = of X T /\ name X /\ {is_sty T}. 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). 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 -> {smember 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. Theorem of_var_inv : forall M L T, ctx L -> {L |- of M T} -> name M -> member (of M T) L. 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. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% 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 -> tm_list -> prop by vars_of_tm_ctx nil snil; vars_of_tm_ctx (tm X :: L) (scons 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. Theorem ctx_mem_to_lst_mem : forall L Vs X T, vars_of_ctx L Vs -> member (of X T) L -> {smember X Vs}. Theorem lst_mem_to_ctx_mem : forall L Vs X, vars_of_ctx L Vs -> {smember X Vs} -> exists T, member (of X T) L. 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. 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. 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_tm to H4. search.Theorem closed_tm_prune : forall M, nabla (x:tm), {tm (M x)} -> exists M', M = y\ M'. 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 -> tm'_list -> prop by vars_of_ctx' nil cnil; vars_of_ctx' (of' X T :: L) (ccons X Vs) := vars_of_ctx' L Vs. Theorem ctx'_islist : forall L, ctx' L -> is_list L. Theorem ctx'_mem : forall E L, ctx' L -> member E L -> exists M T, E = of' M T /\ name' M /\ {is_cty T}. Theorem ctx'_var_mem : forall L T M, ctx' L -> {L |- of' M T} -> name' M -> member (of' M T) L. 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_tm' to H4. case H3. case H1. apply member_prune_tm' 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'. % Lemmas of typing Theorem of'_nat_inv : forall L N T, ctx' L -> {L |- of' (nat' N) T} -> T = tnat. 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. 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_tm'_list FE1. 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 -> tm'_list -> prop by vars_of_tm'_ctx nil cnil; nabla x, vars_of_tm'_ctx (tm' x :: L) (ccons 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'. Theorem tm'_ctx_mem : forall E L, tm'_ctx L -> member E L -> exists X, E = tm' X /\ name' X. 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. % 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_tm' to H4. search.Theorem closed_tm'_prune : forall M, nabla (x:tm'), {tm' (M x)} -> exists M', M = y\ M'. 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 = (ccons 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 = (ccons 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'. 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'.