fact: Fixpoint fresh_inb (x: nat) (t: poly_type) := match t with | poly_var y => if PeanoNat.Nat.eq_dec x y then false else true | poly_arr s t => fresh_inb x s && fresh_inb x t | poly_abs t => fresh_inb (1+x) t end.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun