Fixes #7913: fixpoint with decreasing argument hidden behind a definition - #19296

Fixes #7913: fixpoint with decreasing argument hidden behind a definition#19296

coqbot-app[bot] merged 2 commits into

rocq-prover:masterrocq-prover/rocq:masterfrom

herbelin:master+fixes7913-fixpoint-with-hidden-decreasing-argherbelin/github-coq:master+fixes7913-fixpoint-with-hidden-decreasing-argCopy head branch name to clipboard