proposition: Lemma pure_typing_many_poly_absI {n Gamma M t} : pure_typing (map (ren_poly_type (Nat.add n)) Gamma) M t -> pure_typing Gamma M (many_poly_abs n t).
proof: Proof. have Hnn' : forall Gamma n n', (map (ren_poly_type (Nat.add n')) (map (ren_poly_type (Nat.add n)) Gamma)) = map (ren_poly_type (Nat.add (n + n'))) Gamma. { move=> *. rewrite ?map_map. apply: map_ext => ?. rewrite poly_type_norm /=. apply: extRen_poly_type. by lia. } case: M. - move=> x /pure_typingE [n'] [?] [?] [+] [HC] ->. rewrite Hnn' many_poly_abs_many_poly_abs => ?. apply: (pure_typing_pure_var (n + n')); by eassumption. - move=> ? ? /pure_typingE [n'] [?] [?] [?] [+] [+] [HC] ->. rewrite ?Hnn' many_poly_abs_many_poly_abs => ? ?. apply: (pure_typing_pure_app (n + n')); by eassumption. - move=> ? /pure_typingE [n'] [?] [?] [+] ->. rewrite ?Hnn' many_poly_abs_many_poly_abs => ?. apply: (pure_typing_pure_abs (n + n')); by eassumption. 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