proposition: Lemma subst_poly_type_Pt' {ts t1 t2 t3} : let σ := fold_right scons poly_var ts in subst_poly_type σ (Pt' (length ts) (t1, t2, t3)) = Pt (subst_poly_type σ t1, subst_poly_type σ t2, subst_poly_type σ t3).
proof: Proof. by rewrite /= ?fold_right_length_ts. 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