proposition: Lemma FixWf_unfold_ext `{WF : WellFounded A R} (P : A -> Type) (step : forall x : A, (forall y : A, R y x -> P y) -> P x) (x : A) : FixWf P step x = step x (fun y _ => FixWf P step y).
proof: Proof. intros. unfold FixWf, Fix. destruct wellfounded. simpl. apply ap. apply funext. intros y. apply funext; intros h. apply ap. apply Acc_prop. Qed.
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