fact: Fixpoint last_poly_var (t: poly_type) : option nat := match t with | poly_var x => Some x | poly_arr _ t => last_poly_var t | poly_abs t => if last_poly_var t is Some (S x) then Some x else None end.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun