fact: Fixpoint diagStepR m n (d: diag m n) : diag m (S n) := match d with | diagB => diagS (diagC diagB) | diagC H => diagS (diagC (diagStepR H)) | diagS H => diagS (diagStepR H) end.
imports: FinFun Undecidability.HOU(std.decidable)