proposition: Lemma Fix_step_inv : forall (x:A) (r s:Acc R x), Fix_F R P step _ r = Fix_F R P step _ s.
proof: Proof. intro x; induction (WF x); intros. rewrite <- (Fix_F_eq _ r); rewrite <- (Fix_F_eq _ s); intros. apply step_ext; auto. Defined.
imports: Equations.Init Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties HoTT.Basics.Tactics