proposition: Lemma ext_subst_poly_type_allfv_poly_type {t σ σ'} : allfv_poly_type (fun x => σ x = σ' x) t -> subst_poly_type σ t = subst_poly_type σ' t.
proof: Proof. elim: t σ σ'. - by move=> > /= ->. - by move=> ? IH1 ? IH2 > /= [/IH1 -> /IH2 ->]. - move=> ? IH > /= H. congr poly_abs. apply: IH. apply: iffLR H. apply: ext_allfv_poly_type. case; first done. move=> x /=. rewrite /funcomp. constructor; first by move=> ->. move=> /(congr1 (ren_poly_type Nat.pred)). by rewrite ?poly_type_norm ?ren_poly_type_id. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun