proposition: Lemma Fix_eq : forall x:A, Fix x = step _ (fun (y:A) (p:R y x) => Fix y).
proof: Proof. intro x; unfold Fix. rewrite <- Fix_F_eq. apply step_ext; intros. apply Fix_step_inv. Defined.
imports: Equations.Init Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties HoTT.Basics.Tactics