proposition: Lemma subst_poly_type_h10c_poly_type {ts c} : let σ := (fold_right scons poly_var (rev ts)) in δ = length ts -> subst_poly_type σ (h10c_poly_type c) = match c with | (h10c_one x) => St (σ x, poly_var zt, poly_var (1+zt)) | (h10c_plus x y z) => St (σ x, σ y, σ z) | (h10c_mult x y z) => Pt (σ x, σ y, σ z) end.
proof: Proof. move=> σ Hts. subst σ. case: c. - move=> x. rewrite /= Hts -rev_length ?fold_right_length_ts. have -> : length (rev ts) + 1 + zt = length (rev ts) + (1 + zt) by lia. by rewrite fold_right_length_ts. - move=> >. by rewrite /= Hts -rev_length ?fold_right_length_ts. - move=> >. by rewrite /= Hts -rev_length ?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