proposition: Lemma to_d_typingI s t Gamma : iipc2 Gamma (poly_arr (poly_arr s t) (poly_arr (to_d t) (to_d s))).
proof: Proof. eexists. apply /typing_abs /typing_abs /typing_abs /typing_app. - apply: (typing_var (x := 1)). by reflexivity. - apply: typing_app. + apply: (typing_var (x := 2)). by reflexivity. + apply: (typing_var (x := 0)). by reflexivity. 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