fact: Fixpoint eval (ρ : nat -> tpred) (s : poly_type) : tpred := match s with | poly_var n => Var M (ρ n) | poly_arr s t => Arr M (eval ρ s) (eval ρ t) | poly_abs s => All M (fun d => eval (d .: ρ) s) end.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms