proposition: Lemma pure_typing_K'E {Gamma M N t} : pure_typing Gamma (K' M N) t -> pure_typing Gamma M t /\ pure_typable Gamma N.
proof: Proof. rewrite /K'. move=> /pure_typingE [n] [?] [?] [?] [+] [+] [H1C ->] => /pure_typingE'. move=> /(pure_typing_ren_pure_term_allfv_pure_term Nat.pred (Delta := (map (ren_poly_type (Nat.add n)) Gamma))). apply: unnest. { rewrite allfv_pure_term_ren_pure_term /=. by apply: allfv_pure_term_TrueI. } rewrite renRen_pure_term ren_pure_term_id. move=> /(pure_typing_contains H1C) /pure_typing_many_poly_absI HM. move=> /(pure_typing_ren_poly_type (fun x => x - n)) /pure_typableI HN. constructor; first done. congr pure_typable: HN. rewrite map_map (map_ext _ id). { move=> ?. rewrite ?poly_type_norm ren_poly_type_id' /=; by [|lia]. } apply: map_id. 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 pure_typing_facts) ssreflect ssrbool ssrfun