fact: Definition step_fn_ext {A} {R} (P : A -> Type) := fun step : forall x : A, (forall y : A, R y x -> P y) -> P x => forall x (f g : forall y (H : R y x), P y), (forall y H, f y H = g y H) -> step x f = step x g.
imports: Equations(Init Signature) Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec Equations.Type.Relation Equations.Type.FunctionalExtensionality Equations.Type.WellFounded Equations.Type.DepElim Equations.Type.Constants