Function equation_lemmas 

pub fn equation_lemmas(
    ctx: &Context,
    name: &str,
    ty: &Term,
    body: &Term,
) -> Vec<(String, Term, Term)>

The equation lemmas a definition owes, as (name, statement, proof) in Lean’s order: the unfold theorem first, then one equation per constructor of the matched argument.

★ TWO CANDIDATES MAY SHARE THE NAME <f>_eq_def, IN PREFERENCE ORDER, and generate registers the first the kernel actually CHECKS. This is not indecision; it is the one place where LOGOS’s reduction differs from Lean’s and the difference is visible.

Lean’s unfold theorem is the APPLIED form — dbl.eq_def : ∀ x, dbl x = match x with …, confirmed by #check @dbl.eq_def on this machine — and Lean proves it with a real derivation (Lean/Elab/PreDefinition/Eqns.lean:312 mkUnfoldEq), not with rfl. It cannot be rfl in LOGOS either, and for a sharper reason: reduction.rs’s try_fix_unroll unrolls a fixpoint only when its STRUCTURAL argument is already a constructor, so dbl n for a free n is a normal form and is not convertible with the match it would step to. The applied form is therefore offered first and, where the guard blocks it, the UNAPPLIED dbl = fix dbl. … stands in — true by one δ step, always, and still a name unfold dbl can cite.

Returns an empty vector when there is nothing to state — an equation name, a context with no Eq/refl yet, or a body whose shape carries no equations.