proposition: Lemma pure_typableE {Gamma M} : pure_typable Gamma M -> match M with | pure_var x => if (nth_error Gamma x) is None then False else True | pure_app M N => exists s t, pure_typing Gamma M (poly_arr s t) /\ pure_typing Gamma N s | pure_abs M => exists s, pure_typable (s :: Gamma) M end.
proof: Proof. move=> [t] []. - move=> n {}Gamma x >. rewrite nth_error_map. by case: (nth_error Gamma x). - move=> n > /(pure_typing_ren_poly_type (fun x => x - n)) H1. move=> /(pure_typing_ren_poly_type (fun x => x - n)) H2 _. move: H1 H2. rewrite ?map_map. rewrite (map_ext _ id) ?map_id. { move=> ?. rewrite poly_type_norm ren_poly_type_id' /=; by [|lia]. } move=> ? ?. do 2 eexists. constructor; by eassumption. - move=> n > /(pure_typing_ren_poly_type (fun x => x - n)) /=. rewrite ?map_map. rewrite (map_ext _ id) ?map_id. { move=> ?. rewrite poly_type_norm ren_poly_type_id' /=; by [|lia]. } move=> /pure_typableI ?. eexists. by eassumption. Qed.
imports: List Lia Relation_Definitions Relation_Operators Operators_Properties Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts iipc2_facts) ssreflect ssrbool ssrfun