proposition: Lemma pure_typingE' {Gamma M t} : pure_typing Gamma M t -> match M with | pure_var x => match t with | poly_var _ | poly_arr _ _ => exists s, nth_error Gamma x = Some s /\ contains s t | poly_abs _ => True end | pure_app M N => match t with | poly_var _ | poly_arr _ _ => exists s t', pure_typing Gamma M (poly_arr s t') /\ pure_typing Gamma N s /\ contains t' t | poly_abs _ => True end | pure_abs M => match t with | poly_var _ => False | poly_arr s t => pure_typing (s :: Gamma) M t | poly_abs _ => True end end.
proof: Proof. case: M. - move=> > /pure_typingE [n] [?] [?] [+] []. case: t; last done. all: (case: n; [rewrite map_ren_poly_type_id /=; subst | done]). all: (move=> *; subst; eexists; constructor; by eassumption). - move=> > /pure_typingE [n] [?] [?] [?] [+] [+] []. case: t; last done. all: (case: n; [rewrite map_ren_poly_type_id /=; subst | done]). all: (move=> *; subst; (do 2 eexists); constructor; [| constructor]; by eassumption). - move=> > /pure_typingE [n] [?] [?] []. case: t; last done. all: (case: n; [rewrite map_ren_poly_type_id /=; subst | done]). + done. + move=> > ? [? ?]; by subst. 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