proposition: Lemma transport : H10C_SAT h10cs -> SysF_INH (GammaH, poly_var tt).
proof: Proof. move=> [φ Hφ]. suff: iipc2 GammaH (poly_var tt). { move=> [?] /typing_to_type_assignment ?. eexists; by eassumption. } apply: (introduce_Uts (S (ϵ φ))). apply: (introduce_φ φ Hφ); first by lia. by apply: eliminate_φ. Qed.
imports: PeanoNat List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts term_facts typing_facts iipc2_facts sn_facts) Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun