proposition: Lemma allfv_pure_term_TrueI {p: nat -> Prop} {M} : (forall x, p x) -> allfv_pure_term p M.
proof: Proof. move=> Hp. elim: M. - move=> > /=. by apply: Hp. - by move=> ? + ? + /=. - move=> ? /=. apply: allfv_pure_term_impl. case; first done. move=> *. by apply: Hp. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts Undecidability.SystemF.Util.poly_type_facts ssreflect ssrbool ssrfun