Function parametric_function_ty 

pub fn parametric_function_ty() -> Expr

ParametricFunction : ∀ {F : Type → Type}, (∀ α, F α) → Prop

Predicate: a polymorphic function is parametric if it preserves all relations. ParametricFunction f ↔ ∀ A B (R : Rel A B), Lift_F R (f A) (f B).