proposition: Lemma FixWf_unfold `{WF : WellFounded A R} (P : A -> Type) (step : forall x : A, (forall y : A, R y x -> P y) -> P x) (step_ext : step_fn_ext P step) (x : A) : FixWf P step x = step x (fun y _ => FixWf P step y).
proof: Proof. intros. unfold FixWf. rewrite WellFounded.Fix_eq. - apply step_ext. intros. reflexivity. - intros x' f g H. apply step_ext. apply H. 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)