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