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. Admitted. 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. intros. rewrite FixWf_unfold, X. reflexivity. apply step_ext. 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