proposition: Lemma Fix_F_eq : forall (x:A) (r:Acc R x), step _ (fun (y:A) (p:R y x) => Fix_F R P step y (Acc_inv R r _ p)) = Fix_F R P step x r.
proof: Proof. destruct r; reflexivity. Defined.
imports: Equations.Init Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties HoTT.Basics.Tactics