proposition: Lemma allfv_poly_type_allfv_poly_type_impl {P1 P2: nat -> Prop} {t}: allfv_poly_type (fun x => P1 x -> P2 x) t -> allfv_poly_type P1 t -> allfv_poly_type P2 t.
proof: Proof. elim: t P1 P2. - done. - move=> ? IH1 ? IH2 > /= [/IH1 {}IH1 /IH2 {}IH2] [/IH1 ? /IH2 ?]. by constructor. - move=> ? IH > /= H. apply: IH. apply: allfv_poly_type_impl H. by case. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun