proposition: Lemma pure_typingE {Gamma M t} : pure_typing Gamma M t -> match M with | pure_var x => exists n s t', nth_error (map (ren_poly_type (Nat.add n)) Gamma) x = Some s /\ contains s t' /\ t = many_poly_abs n t' | pure_app M N => exists n s t' t'', pure_typing (map (ren_poly_type (Nat.add n)) Gamma) M (poly_arr s t') /\ pure_typing (map (ren_poly_type (Nat.add n)) Gamma) N s /\ contains t' t'' /\ t = many_poly_abs n t'' | pure_abs M => exists n s t', pure_typing (s :: map (ren_poly_type (Nat.add n)) Gamma) M t' /\ t = many_poly_abs n (poly_arr s t') end.
proof: Proof. case => *; [do 3 eexists | do 4 eexists | do 3 eexists]; by eauto. 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