proposition: Lemma pure_typable_self_application {Gamma x n t} : not (is_poly_abs t) -> nth_error Gamma x = Some (many_poly_abs n t) -> pure_typable Gamma (pure_app (pure_var x) (pure_var x)) -> exists y, y < n /\ leftmost_poly_var t = Some y.
proof: Proof. move=> Ht Hx /pure_typableE [?] [?] []. move=> /pure_typingE' [?] []. rewrite Hx => [[<-]] H1C. move=> /pure_typingE [n3] [?] [s'] [+] []. rewrite nth_error_map Hx => [[?]] H2C ?. subst. move: Ht H1C H2C. clear => Ht + /contains_ren_poly_type_addLR. move=> /contains_leftmost_path_length_eq + /contains_leftmost_path_length_eq. move=> /(_ Ht) + /(_ Ht). case: (leftmost_poly_var t). - move=> y H1y H2y. exists y. constructor; last done. suff: (not (n <= y)) by lia. move=> /[dup] [/H1y + /H2y] => -> /=. rewrite leftmost_path_length_many_poly_abs leftmost_path_length_ren_poly_type. by lia. - move=> -> /=. rewrite leftmost_path_length_many_poly_abs leftmost_path_length_ren_poly_type. by lia. 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