proposition: Lemma FixWf_unfold_step : forall (A : Type) (R : Relation A) (WF : WellFounded R) (P : A -> Type) (step : forall x : A, (forall y : A, R y x -> P y) -> P x) (x : A) (step_ext : step_fn_ext P step) (step' : forall y : A, R y x -> P y), step' = (fun (y : A) (_ : R y x) => FixWf P step y) -> FixWf P step x = step x step'.
proof: Proof. intros. rewrite FixWf_unfold, X. - reflexivity. - apply step_ext. Defined.
imports: Equations(Init Signature) Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.Relation Equations.HoTT.WellFounded Equations.HoTT.DepElim Equations.HoTT.Constants HoTT(Basics.Tactics Spaces.Nat)