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 Init.Wf.Fix_eq. apply step_ext. intros. reflexivity. intros x' f g H. apply step_ext. apply H. Qed.
imports: Coq(Wf_nat Relations) Coq(Wellfounded Relation_Definitions) Coq(Relation_Operators Lexicographic_Product Wf_nat) Equations(Init Signature) Equations.CoreTactics Equations.Prop.Classes Equations.Prop.EqDec Equations.Prop.DepElim Equations.Prop.Constants