proposition: Lemma typingE {Gamma P t} : typing Gamma P t -> match P with | var x => nth_error Gamma x = Some t | app P Q => exists s, typing Gamma P (poly_arr s t) /\ typing Gamma Q s | abs s P => exists t', t = poly_arr s t' /\ typing (s :: Gamma) P t' | ty_app P t' => exists s, t = (subst_poly_type (t' .: poly_var) s) /\ typing Gamma P (poly_abs s) | ty_abs P => exists s, t = (poly_abs s) /\ typing (map (ren_poly_type S) Gamma) P s end.
proof: Proof. case; by eauto. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts term_facts) ssreflect ssrbool ssrfun