proposition: Lemma pure_typable_pure_app_0_0' {n1 n2 n3 n4 x y n5 s t Gamma}: pure_typable (many_poly_abs n1 (poly_arr (many_poly_abs n2 (poly_arr (many_poly_abs n3 (poly_var (n3 + (n2 + x)))) (many_poly_abs n4 (poly_var y)))) (many_poly_abs n5 (poly_arr s t))) :: Gamma) (pure_app (pure_var 0) (pure_var 0)) -> exists y', y = n4 + (n2 + y').
proof: Proof. move=> /pure_typableE [?] [?] [/pure_typingE'] [?] [[?]] H1c. subst. move=> /pure_typingE [n6] [?] [?] [[?]] [H2c ?]. subst. move: H1c => /contains_poly_arrE [?] [?] /= [+ ?]. subst. set σ := (fold_right _ _ _). rewrite subst_poly_type_many_poly_abs /=. move=> /many_poly_abs_eqE'' => /(_ ltac:(done)) [n7] [? ?]. subst. move: H2c. rewrite ren_poly_type_many_poly_abs /=. move=> /contains_sub' [_]. rewrite ren_poly_type_many_poly_abs /= many_poly_abs_many_poly_abs. move=> /contains_sub [?] [?] [?] [+] _. rewrite subst_poly_type_many_poly_abs /= many_poly_abs_many_poly_abs. move=> /many_poly_abs_eqE'' => /(_ ltac:(done)) [n8] [+ ?]. subst. have [?|?] : y < n4 + n6 + n7 \/ n4 + n6 + n7 <= y by lia. - rewrite iter_plus iter_up_poly_type_poly_type_lt; first by lia. by case: n8. - move=> _. exists (y - n4 - n6 - n7). 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