proposition: Lemma fresh_inP {x t} : reflect (fresh_in x t) (fresh_inb x t).
proof: Proof. elim: t x. - move=> n x. rewrite /=. case: (PeanoNat.Nat.eq_dec _ _). + move=> /= ->. by constructor. + move=> /= ?. by constructor. - move=> ? IH1 ? IH2 x /=. rewrite /fresh_in /= -?/(fresh_in _ _). apply /introP; rewrite (rwP (IH1 x)) (rwP (IH2 x)). + by case: (fresh_inb _ _); case (fresh_inb _ _). + case: (fresh_inb _ _); case (fresh_inb _ _); by move=> ? [? ?]. - move=> t IH x. rewrite /fresh_in /= -?/(fresh_in _ _). apply /introP. + rewrite -(rwP (IH (S x))). apply: allfv_poly_type_impl. case; [done | by move=> /= *; lia]. + have := (rwP (IH (S x))). case: (fresh_inb (S x) t); first done. move=> H _ H'. suff: false by done. apply /H. apply: allfv_poly_type_impl H'. case; [done | by move=> /= *; lia]. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun