fact: Definition C (Γ : nat -> poly_type) (ρ : nat -> tpred) : (nat -> term) -> Prop := fun σ => forall n, E (Γ n) ρ (σ n).
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms