Click on a command or tactic to see a detailed view of its use.
Specification "trans". Import "typing". [View typing] % Definition and lemmas for fvars Define prune_ctx : list tm -> olist -> olist -> prop by prune_ctx nil L nil; prune_ctx (X :: Vs) L (of X T :: L') := member (of X T) L /\ prune_ctx Vs L L'. Define bvars : olist -> prop by bvars nil; nabla x, bvars (notfree x :: L) := bvars L. Define ctx_bvars : olist -> olist -> prop by ctx_bvars nil nil; ctx_bvars (of X T :: L) (notfree X :: L') := ctx_bvars L L'. Theorem bvars_mem : forall BVs E, bvars BVs -> member E BVs -> exists X, E = notfree X /\ name X. Theorem prune_ctx_mem_rev : forall FVs L L' A, prune_ctx FVs L L' -> member A L' -> member A L. Theorem prune_ctx_pres : forall FVs L L', ctx L -> prune_ctx FVs L L' -> ctx L'.induction on 2. intros. case H2. search. apply IH to _ H4. apply ctx_mem to _ H3. unfold. search. search. search. intros. apply prune_ctx_mem_rev to H4 H8. backchain ctx_mem_sync.Theorem prune_ctx_vars_of : forall FVs L L', prune_ctx FVs L L' -> vars_of_ctx L' FVs. Theorem ctx_bvars_sync : forall X L Ps, ctx_bvars L Ps -> member (notfree X) Ps -> exists T, member (of X T) L. Theorem subset_prune_ctx : forall L L' Vs, subset L L' -> vars_of_ctx L Vs -> prune_ctx Vs L' L. Theorem memb_bvars_strengthening : forall Ps (M:tm) Vs, bvars Ps -> {Ps |- memb M Vs} -> {memb M Vs}.induction on 2. intros. case H2. search. assert {memb M L}. backchain IH. search. apply bvars_mem to _ H4. case H3.Theorem combine_bvars_strengthening : forall (L1:list tm) L2 L3 Ps, bvars Ps -> {Ps |- combine L1 L2 L3} -> {combine L1 L2 L3}.induction on 2. intros. case H2. search. apply IH to H1 H4. apply memb_bvars_strengthening to H1 H3. search. apply IH to H1 H3. search. apply bvars_mem to H1 H4. case H3.Theorem ctx_vars_of_ctx_sync : forall L Vs X, ctx L -> vars_of_ctx L Vs -> {memb X Vs} -> exists T, member (of X T) L.induction on 3. intros. case H3. case H2. case H1. search. case H2. case H1. apply IH to _ _ H4. search.Theorem prune_ctx_prune_tm : forall FVs L L', nabla (n:tm), prune_ctx FVs L (L' n) -> exists L'', L' = y\L''. Theorem prune_ctx_input_islist : forall Vs L L', prune_ctx Vs L L' -> is_list Vs. Theorem prune_ctx_rsl_islist : forall Vs L L', prune_ctx Vs L L' -> is_list L'. Theorem prune_ctx_rsl_subset : forall Vs L L', prune_ctx Vs L L' -> subset L' L. Theorem prune_ctx_exists : forall X Vs L L', {memb X Vs} -> prune_ctx Vs L L' -> exists T, member (of X T) L'. Theorem subset_prune_ctx_sim : forall Vs1 Vs2 L L1 L2, ctx L -> ssubset Vs1 Vs2 -> prune_ctx Vs1 L L1 -> prune_ctx Vs2 L L2 -> subset L1 L2.induction on 3. intros. case H3. search. case H2. unfold. apply prune_ctx_exists to H7 H4. apply prune_ctx_mem_rev to H4 H9. apply ctx_mem_sync to _ H5 H10. search. backchain IH.Theorem prune_ctx_combine : forall Vs1 Vs2 L L1 L2 Vs, prune_ctx Vs1 L L1 -> prune_ctx Vs2 L L2 -> {combine Vs1 Vs2 Vs} -> exists L', prune_ctx Vs L L'.induction on 3. intros. case H3. case H1. search. case H1. assert exists L', prune_ctx Vs L L'. backchain IH with Vs1 = L5. case H8. search. case H1. assert exists L', prune_ctx L3 L L'. backchain IH with Vs1 = L5, Vs2 = Vs2, Vs = L3. case H7. search.Theorem ctx_prune_tail : forall L LH LT FVs LT' L', ctx L -> append LH LT L -> prune_ctx FVs LT LT' -> append LH LT' L' -> ctx L'.induction on 2. intros. case H2. case H4. backchain prune_ctx_pres. case H4. case H1. apply IH to _ H5 H3 _. unfold. search. search. search. intros. backchain H10. backchain subset_mem_trans with L1 = L5. backchain append_append_subset_trans with L1 = L1, L1' = L1, L2 = LT', L2' = LT. backchain append_arg2_islist with L1 = L1, L = L3. backchain ctx_islist. backchain subset_refl. backchain append_arg1_islist. backchain prune_ctx_rsl_subset.Theorem combine_prune_tail_ctx : forall L LH LT FVs1 LT1 FVs2 LT2 FVs, ctx L -> append LH LT L -> prune_ctx FVs1 LT LT1 -> prune_ctx FVs2 LT LT2 -> {combine FVs1 FVs2 FVs} -> exists LF LT', prune_ctx FVs LT LT' /\ append LH LT' LF /\ ctx LF.intros. assert exists LT', prune_ctx FVs LT LT'. backchain prune_ctx_combine with Vs1 = FVs1, Vs2 = FVs2. case H6. assert exists LF, append LH LT' LF. backchain append_exists[o]. backchain append_arg1_islist. case H8. assert ctx LF. backchain ctx_prune_tail with L = L, LH = LH, LT = LT, LT' = LT'. search.Theorem prune_typing_weakening : forall FVs1 FVs2 LT LT1 LT2 LH LF1 LF2 M T, ctx LT -> ctx LF1 -> ssubset FVs1 FVs2 -> prune_ctx FVs1 LT LT1 -> prune_ctx FVs2 LT LT2 -> append LH LT1 LF1 -> {LF1 |- of M T} -> append LH LT2 LF2 -> {LF2 |- of M T}.intros. assert subset LT1 LT2. backchain subset_prune_ctx_sim with Vs1 = FVs1, Vs2 = FVs2, L = LT. assert subset LF1 LF2. backchain append_append_subset_trans with L1 = LH, L1' = LH, L2 = LT1, L2' = LT2. backchain prune_ctx_rsl_islist. backchain subset_refl. backchain append_arg1_islist. backchain of_weakening with L = LF1.Theorem prune_typing_pres : forall L L1 L2 Ps Vs FVs M T, ctx L -> append L1 L2 L -> ctx_bvars L1 Ps -> vars_of_ctx L2 Vs -> bvars Ps -> {Ps |- fvars M Vs FVs} -> {L |- of M T} -> exists L' L2', prune_ctx FVs L2 L2' /\ append L1 L2' L' /\ ctx L' /\ {L' |- of M T}.induction on 6. intros. case H6. % M is not free exists L1. exists nil. split. search. backchain append_refl. backchain append_arg1_islist. backchain ctx_subset. backchain append_sub1. case H8. apply bvars_mem to _ H10. case H9. apply ctx_bvars_sync to _ H10. apply append_sub1 to H2. apply subset_mem_trans to H13 H12. case H11. case H7. apply ctx_mem to _ H16. case H15. apply ctx_mem_sync to _ H14 H16. search. % M is free apply memb_bvars_strengthening to _ H8. apply ctx_vars_of_ctx_sync to _ H4 _. backchain ctx_subset with L = L. backchain append_sub2. backchain append_arg2_islist with L1 = L1, L = L. backchain ctx_islist. assert exists L', append L1 (of M T1 :: nil) L'. backchain append_exists[o]. backchain append_arg1_islist. case H11. assert subset L2 L. backchain append_sub2. backchain append_arg2_islist with L1 = L1, L = L. backchain ctx_islist. assert member (of M T1) L. backchain subset_mem_trans with L1 = L2. exists L'. exists (of M T1 :: nil). split. search. search. backchain ctx_subset with L = L. backchain append_subset_trans with L1 = L1, L2 = (of M T1 :: nil). backchain append_sub1. apply ctx_name to _ _ H9. backchain ctx_subset with L = L. case H15. case H7. apply ctx_mem to _ H17. case H16. apply ctx_mem_sync to _ H14 H17. apply append_sub2 to _ H12. case H20. search. % M = nat case H7. exists L1. exists nil. split. search. backchain append_refl. backchain append_arg1_islist. backchain ctx_subset. backchain append_sub1. search. % Context case apply ctx_focus_inv to _ H9 H8. case H10. % M = spred M1 case H7. apply IH to _ _ _ _ _ H8 H9. search. % Context case apply ctx_focus_inv to _ H10 H9. case H11. % M = (splus M1 M2) case H7. assert exists L'1 L2'1, prune_ctx FVs1 L2 L2'1 /\ append L1 L2'1 L'1 /\ ctx L'1 /\ {L'1 |- of M1 tnat}. backchain IH. case H13. assert exists L'2 L2'2, prune_ctx FVs2 L2 L2'2 /\ append L1 L2'2 L'2 /\ ctx L'2 /\ {L'2 |- of M2 tnat}. backchain IH. case H18. assert {combine FVs1 FVs2 FVs}. backchain combine_bvars_strengthening. assert exists L' L2', prune_ctx FVs L2 L2' /\ append L1 L2' L' /\ ctx L'. backchain combine_prune_tail_ctx with FVs2 = FVs2. case H24. assert ctx L2. backchain ctx_subset. backchain append_sub2. backchain append_arg2_islist with L1 = L1, L = L. backchain ctx_islist. assert {L' |- of M1 tnat}. backchain prune_typing_weakening with FVs1 = FVs1, FVs2 = FVs, LT = L2, LT1 = L2'1, LT2 = L2', LH = L1, LF1 = L'1. backchain combine_sub1. backchain prune_ctx_input_islist. assert {L' |- of M2 tnat}. backchain prune_typing_weakening with FVs1 = FVs2, FVs2 = FVs, LT = L2, LT1 = L2'2, LT2 = L2', LH = L1, LF1 = L'2. backchain combine_sub2.backchain prune_ctx_input_islist. search. % Context case apply ctx_focus_inv to _ H12 H11. case H13. % M = ifz M3 M1 M2. case H7. assert exists L'3 L2'3, prune_ctx FVs3 L2 L2'3 /\ append L1 L2'3 L'3 /\ ctx L'3 /\ {L'3 |- of M3 tnat}. backchain IH. case H16. assert exists L'1 L2'1, prune_ctx FVs1 L2 L2'1 /\ append L1 L2'1 L'1 /\ ctx L'1 /\ {L'1 |- of M1 T}. backchain IH. case H21. assert exists L'2 L2'2, prune_ctx FVs2 L2 L2'2 /\ append L1 L2'2 L'2 /\ ctx L'2 /\ {L'2 |- of M2 T}. backchain IH. case H26. % Weakening the typing derivation for the conditional expression and the % expression in the them branch assert {combine FVs3 FVs1 FVs1'}. backchain combine_bvars_strengthening. assert exists L' L2', prune_ctx FVs1' L2 L2' /\ append L1 L2' L' /\ ctx L'. backchain combine_prune_tail_ctx with FVs2 = FVs1. case H32. assert ctx L2. backchain ctx_subset. backchain append_sub2. backchain append_arg2_islist with L1 = L1, L = L. backchain ctx_islist. assert {L' |- of M3 tnat}. backchain prune_typing_weakening with FVs1 = FVs3, FVs2 = FVs1', LT = L2, LT1 = L2'3, LT2 = L2', LH = L1, LF1 = L'3. backchain combine_sub1. backchain prune_ctx_input_islist. assert {L' |- of M1 T}. backchain prune_typing_weakening with FVs1 = FVs1, FVs2 = FVs1', LT = L2, LT1 = L2'1, LT2 = L2', LH = L1, LF1 = L'1. backchain combine_sub2. backchain prune_ctx_input_islist. % Weakening the typing derivation for all the expressions assert {combine FVs1' FVs2 FVs}. backchain combine_bvars_strengthening. assert exists L'' L2'', prune_ctx FVs L2 L2'' /\ append L1 L2'' L'' /\ ctx L''. backchain combine_prune_tail_ctx with FVs1 = FVs1', FVs2 = FVs2. case H40. assert {L'' |- of M3 tnat}. backchain prune_typing_weakening with FVs1 = FVs1', FVs2 = FVs, LT = L2, LT1 = L2', LT2 = L2'', LH = L1, LF1 = L'. backchain combine_sub1. backchain prune_ctx_input_islist. assert {L'' |- of M1 T}. backchain prune_typing_weakening with FVs1 = FVs1', FVs2 = FVs, LT = L2, LT1 = L2', LT2 = L2'', LH = L1, LF1 = L'. backchain combine_sub1. backchain prune_ctx_input_islist. assert {L'' |- of M2 T}. backchain prune_typing_weakening with FVs1 = FVs2, FVs2 = FVs, LT = L2, LT1 = L2'2, LT2 = L2'', LH = L1, LF1 = L'2. backchain combine_sub2. backchain prune_ctx_input_islist. search. % Context case apply ctx_focus_inv to _ H14 H13. case H15. % M = sul case H7. exists L1. exists nil. split. search. backchain append_refl. backchain append_arg1_islist. backchain ctx_subset with L = L. backchain append_sub1. search. % Context case apply ctx_focus_inv to _ H9 H8. case H10. % M = spair M1 M2. case H7. assert exists L'1 L2'1, prune_ctx FVs1 L2 L2'1 /\ append L1 L2'1 L'1 /\ ctx L'1 /\ {L'1 |- of M1 T1}. backchain IH. case H13. assert exists L'2 L2'2, prune_ctx FVs2 L2 L2'2 /\ append L1 L2'2 L'2 /\ ctx L'2 /\ {L'2 |- of M2 T2}. backchain IH. case H18. assert {combine FVs1 FVs2 FVs}. backchain combine_bvars_strengthening. assert exists L' L2', prune_ctx FVs L2 L2' /\ append L1 L2' L' /\ ctx L'. backchain combine_prune_tail_ctx with FVs2 = FVs2. case H24. assert ctx L2. backchain ctx_subset. backchain append_sub2. backchain append_arg2_islist with L1 = L1, L = L. backchain ctx_islist. assert {L' |- of M1 T1}. backchain prune_typing_weakening with FVs1 = FVs1, FVs2 = FVs, LT = L2, LT1 = L2'1, LT2 = L2', LH = L1, LF1 = L'1. backchain combine_sub1. backchain prune_ctx_input_islist. assert {L' |- of M2 T2}. backchain prune_typing_weakening with FVs1 = FVs2, FVs2 = FVs, LT = L2, LT1 = L2'2, LT2 = L2', LH = L1, LF1 = L'2. backchain combine_sub2. backchain prune_ctx_input_islist. search. % Context case apply ctx_focus_inv to _ H12 H11. case H13. % M = sfst M1 case H7. apply IH to _ _ _ _ _ H8 H9. search. % Context case apply ctx_focus_inv to _ H10 H9. case H11. % M = ssndM1 case H7. apply IH to _ _ _ _ _ H8 H9. search. % Context case apply ctx_focus_inv to _ H10 H9. case H11. % M = slet M1 R case H7. assert exists L'1 L2'1, prune_ctx FVs1 L2 L2'1 /\ append L1 L2'1 L'1 /\ ctx L'1 /\ {L'1 |- of M1 T1}. backchain IH. case H13. apply IH to _ _ _ _ _ H9 H12. backchain ctx_extend. backchain of_is_sty. assert {combine FVs1 FVs2 FVs}. backchain combine_bvars_strengthening. assert exists L' L2', prune_ctx FVs L2 L2' /\ append L1 L2' L' /\ ctx L'. backchain combine_prune_tail_ctx with FVs1 = FVs1, FVs2 = FVs2, LT1 = L2'1, LT2 = L2' n1. case H23. assert ctx L2. backchain ctx_subset. backchain append_sub2. backchain append_arg2_islist with L1 = L1, L = L. backchain ctx_islist. assert {L'2 |- of M1 T1}. backchain prune_typing_weakening with FVs1 = FVs1, FVs2 = FVs, LT = L2, LT1 = L2'1, LT2 = L2'2, LH = L1, LF1 = L'1. backchain combine_sub1. backchain prune_ctx_input_islist. apply prune_typing_weakening to _ _ _ H18 H24 H19 H21 _. backchain combine_sub2. backchain prune_ctx_input_islist. search. % Context case apply ctx_focus_inv to _ H12 H11. case H13. % M = sfix R case H7. apply IH to _ _ _ _ _ H8 H9. apply is_sty_str to _ H10. case H11. backchain ctx_extend. backchain ctx_extend. case H12. case H15. apply prune_ctx_prune_tm to H11. apply prune_ctx_prune_tm to H11. apply append_prune to H16. apply append_prune to H16. case H13. case H17. search. % Context case apply ctx_focus_inv to _ H10 H9. case H11. % M = sapp M1 M2 case H7. assert exists L'1 L2'1, prune_ctx FVs1 L2 L2'1 /\ append L1 L2'1 L'1 /\ ctx L'1 /\ {L'1 |- of M1 (arr T1 T)}. backchain IH. case H13. assert exists L'2 L2'2, prune_ctx FVs2 L2 L2'2 /\ append L1 L2'2 L'2 /\ ctx L'2 /\ {L'2 |- of M2 T1}. backchain IH. case H18. assert {combine FVs1 FVs2 FVs}. backchain combine_bvars_strengthening. assert exists L' L2', prune_ctx FVs L2 L2' /\ append L1 L2' L' /\ ctx L'. backchain combine_prune_tail_ctx with FVs2 = FVs2. case H24. assert ctx L2. backchain ctx_subset. backchain append_sub2. backchain append_arg2_islist with L1 = L1, L = L. backchain ctx_islist. assert {L' |- of M1 (arr T1 T)}. backchain prune_typing_weakening with FVs1 = FVs1, FVs2 = FVs, LT = L2, LT1 = L2'1, LT2 = L2', LH = L1, LF1 = L'1. backchain combine_sub1. backchain prune_ctx_input_islist. assert {L' |- of M2 T1}. backchain prune_typing_weakening with FVs1 = FVs2, FVs2 = FVs, LT = L2, LT1 = L2'2, LT2 = L2', LH = L1, LF1 = L'2. backchain combine_sub2.backchain prune_ctx_input_islist. search. % Context case apply ctx_focus_inv to _ H12 H11. case H13. % Context case. apply bvars_mem to _ H9. case H8.Theorem fvars_typing_pres : forall L Vs M T FVs, ctx L -> vars_of_ctx L Vs -> {L |- of M T} -> {fvars M Vs FVs} -> exists L', prune_ctx FVs L L' /\ {L' |- of M T}. % Well-formedness of terms is preserved under closure conversion Define good_map : olist -> list (map tm tm') -> olist -> prop by good_map CL nil nil; good_map CL (map X M :: ML) (of X T :: SL) := name X /\ {CL |- of' M T} /\ good_map CL ML SL. Theorem good_map_name : forall CL Map SL X M, good_map CL Map SL -> {memb (map X M) Map} -> name X. Theorem good_map_of' : forall CL Map SL M X, good_map CL Map SL -> {memb (map X M) Map} -> exists T, member (of X T) SL /\ {CL |- of' M T}. Theorem good_map_extend_ctx' : forall SL CL Map Y T, good_map CL Map SL -> good_map (of' Y T :: CL) Map SL. Theorem good_map_extend_map : forall CL Map SL X Y T, good_map CL Map SL -> name X -> good_map (of' Y T :: CL) (map X Y :: Map) (of X T :: SL). Theorem good_map_csnd : forall M SL X T RT, good_map (of' (snd' X) RT :: nil) M SL -> good_map (of' X (prod T RT) :: nil) M SL.induction on 1. intros. case H1. search. assert {of' X (prod T RT) |- of' (snd' X) RT}. cut H3 with H5. apply IH to H4 with T = T. search.% Definition and lemmas for reifying a type environment Define reified_env : olist -> ty -> prop by reified_env nil tunit; reified_env (of X T :: SL) (prod T RT) := reified_env SL RT. Theorem reified_env_sty : forall L T, ctx L -> reified_env L T -> {is_sty T}. Theorem reified_env_exists : forall SL, ctx SL -> exists Ty, reified_env SL Ty. % One part of the reification lemma: mapvar specifies a type preserving % mapping with respect to type of the reified environment. Theorem reify_mapvar_env : forall FVs SL RTy Map X, vars_of_ctx SL FVs -> ctx SL -> {mapvar FVs Map} -> reified_env SL RTy -> good_map (of' X RTy :: nil) (Map X) SL.induction on 1. intros. case H1. case H3. search. case H3. case H4. unfold. case H2. search. search. case H2. apply IH to H5 _ H6 _ with X = (snd' X). apply good_map_csnd to H12 with T = T. search.% The other part of the reification lemma: mapenv reifies the environment % in a way that matches the reified type. Theorem pruned_env_reification_env : forall CL Map SL SL' Ty PE FVs, ctx SL -> good_map CL Map SL -> prune_ctx FVs SL SL' -> reified_env SL' Ty -> {mapenv FVs Map PE} -> {CL |- of' PE Ty}.induction on 3. intros. case H3. case H4. case H5. search. case H4. case H5. assert {CL |- of' M T}. apply good_map_of' to H2 H9. apply ctx_mem_sync to _ H6 H11. search. assert {CL |- of' ML RT}. backchain IH. search.Theorem cc_typ_pres : forall SL CL Map M Vs M' T, ctx SL -> ctx' CL -> good_map CL Map SL -> {SL |- of M T} -> vars_of_ctx SL Vs -> {cc Map Vs M M'} -> {CL |- of' M' T}.induction on 6. intros. case H6. % M = nat N case H4. search. % Context case apply ctx_focus_inv to _ H8 H7. case H9. % M is a variable apply good_map_of' to _ H7. apply good_map_name to _ H7. case H10. case H4. apply ctx_mem to _ H12. case H11. apply ctx_mem_sync to _ H8 H12. search. % M = pred M1 case H4. assert {CL |- of' M'1 tnat}. backchain IH. search. % Context case apply ctx_focus_inv to _ H9 H8. case H10. % M = plus M1 M2 case H4. assert {CL |- of' M1' tnat}. backchain IH. assert {CL |- of' M2' tnat}. backchain IH with M = M2. search. % Context case apply ctx_focus_inv to _ H10 H9. case H11. % M = ifz M3 M1 M2 case H4. assert {CL |- of' M'1 tnat}. backchain IH. assert {CL |- of' M1' T}. backchain IH with M = M1. assert {CL |- of' M2' T}. backchain IH with M = M2. search. % Context case apply ctx_focus_inv to _ H11 H10. case H12. % M = unit case H4. search. % Context case apply ctx_focus_inv to _ H8 H7. case H9. % M = pair M1 M2 case H4. assert {CL |- of' M1' T1}. backchain IH. assert {CL |- of' M2' T2}. backchain IH with M = M2. search. % Context case apply ctx_focus_inv to _ H10 H9. case H11. % M = fst M1 case H4. assert {CL |- of' M'1 (prod T T2)}. backchain IH. search. % Context case apply ctx_focus_inv to _ H9 H8. case H10. % M = snd M1 case H4. assert {CL |- of' M'1 (prod T1 T)}. backchain IH. search. % Context case apply ctx_focus_inv to _ H9 H8. case H10. % M = let M1 R case H4. assert {CL |- of' M'1 T1}. backchain IH. assert {CL, of' n2 T1 |- of' (R' n2) T}. backchain IH with M = (R n1), SL = (of n1 T1 :: SL), Map = map n1 n2 :: Map, Vs = n1 :: Vs. backchain ctx_extend. backchain of_is_sty. apply of_is_sty to _ H9. apply sty_to_cty to H12. search. backchain good_map_extend_map. search. % Context case apply ctx_focus_inv to _ H10 H9. case H11. % M = fix R assert exists SL', prune_ctx FVs SL SL' /\ {SL' |- of M T}. backchain fvars_typing_pres. case H11. case H13. apply prune_ctx_pres to _ H12. apply reified_env_exists to H16. assert {CL |- of' E Ty}. backchain pruned_env_reification_env. assert good_map (of' n4 T1 :: of' n3 (arr T1 T2) :: of' n5 Ty :: nil) (map n2 n4 :: map n1 n3 :: (NMap n5)) (of n2 T1 :: of n1 (arr T1 T2) :: SL'). backchain good_map_extend_map. backchain good_map_extend_map. backchain reify_mapvar_env with Map = NMap. backchain prune_ctx_vars_of. apply is_sty_str to _ H15. case H20. assert {of' n5 Ty, of' n3 (arr T1 T2), of' n4 T1 |- of' (R' n3 n4 n5) T2}. backchain IH with SL = (of n2 T1 :: of n1 (arr T1 T2) :: SL'), M = (R n1 n2), Map = (map n2 n4 :: map n1 n3 :: (NMap n5)), Vs = (n2 :: n1 :: FVs). backchain ctx_extend. backchain ctx_extend. apply sty_to_cty to H21. apply sty_to_cty to H22. apply reified_env_sty to _ H17. apply sty_to_cty to H25. search. unfold. unfold. backchain prune_ctx_vars_of. apply sty_to_cty to H21. apply sty_to_cty to H22. apply reified_env_sty to _ H17. apply sty_to_cty to H26. assert {of' (abs' (p\let' (fst' p) (g\let' (fst' (snd' p)) (y\let' (snd' (snd' p)) (e\R' g y e))))) (arr' (prod (arr T1 T2) (prod T1 Ty)) T2)}. search 7. search. % Context case assert ctx SL'. backchain prune_ctx_pres. apply ctx_focus_inv to _ H15 H14. case H17. % M = app M1 M2 case H4. assert {CL |- of' M1' (arr T1 T)}. backchain IH. assert {CL |- of' M2' T1}. backchain IH. search. % Context case apply ctx_focus_inv to _ H10 H9. case H11.Theorem cc_clos_code_typ_pres : forall SL Ty T1 T2 R FVs Map R', nabla f x g y e, ctx SL -> reified_env SL Ty -> {is_sty (arr T1 T2)} -> {SL, of f (arr T1 T2), of x T1 |- of (R f x) T2} -> vars_of_ctx SL FVs -> {mapvar FVs Map} -> {cc (map x y :: map f g :: (Map e)) (x :: f :: FVs) (R f x) (R' g y e)} -> {of' e Ty, of' g (arr T1 T2), of' y T1 |- of' (R' g y e) T2}.intros. assert good_map (of' n4 T1 :: of' n3 (arr T1 T2) :: of' n5 Ty :: nil) (map n2 n4 :: map n1 n3 :: Map n5) (of n2 T1 :: of n1 (arr T1 T2) :: SL). backchain good_map_extend_map. backchain good_map_extend_map. backchain reify_mapvar_env with Map = Map. backchain cc_typ_pres with SL = (of n2 T1 :: of n1 (arr T1 T2) :: SL), M = (R n1 n2), Map = (map n2 n4 :: map n1 n3 :: Map n5), Vs = (n2 :: n1 :: FVs). backchain ctx_extend. backchain ctx_extend. case H3. search. case H3. apply sty_to_cty to H9. apply sty_to_cty to H10. apply reified_env_sty to _ H2. apply sty_to_cty to H13. search.Theorem cc_typ_pres_closed : forall M M' T, {of M T} -> {cc' M M'} -> {of' M' T}.