fact: Fixpoint is_simple (t: poly_type) := match t with | poly_var _ => True | poly_arr s t => is_simple s /\ is_simple t | poly_abs _ => False end.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun