proposition: Lemma transport : SysF_TYP M0 -> SysF_TC (Gamma_M0, M_M0, t_M0).
proof: Proof. move=> [Gamma] [t] /pure_typing_iff_type_assignment. move=> /pure_typableI /pure_typable_many_pure_term_abs_allI [{}t]. move=> /(pure_typing_ren_pure_term id (Delta := Gamma_M0)). rewrite ren_pure_term_id. apply: unnest; first by case. move=> /(pure_typing_pure_app_simpleI (M := pure_var 0) (t := t_M0)). apply: unnest. { apply: (pure_typing_pure_var 0); first by reflexivity. apply: rt_step. by apply: contains_step_subst. } move=> /pure_typing_to_typing /= [P] [HP] /typing_to_type_assignment. by rewrite -HP. Qed.
imports: List Lia Relation_Operators Undecidability.SystemF.SysF Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts pure_typing_facts) ssreflect ssrbool ssrfun