fact: Record is_cand (X : term -> Prop) : Prop := {incl_sn : forall t : term, X t -> sn t; clos_red : forall t : term, X t -> forall u : term, red1 t u -> X u; clos_exp : forall t : term, neutral t -> (forall u : term, red1 t u -> X u) -> X t}.
imports: Termes Conv Types Class