fact: Definition well_founded_restriction_rect : well_founded_restriction -> forall X : A -> Type, (forall x : A, E x -> (forall y : A, In _ E y -> R y x -> X y) -> X x) -> forall a : A, In _ E a -> X a.
imports: Coq(Wellfounded Ensembles Relations)