▽天泣記 ●03/22 12:45 2025-03-20 (Thu)#1 あみだくじ (2)証明の場合分けが不必要に多かったので減らしてみた。(他にもいくらか調整した。)From mathcomp Require Import all_ssreflect.Section amida_kuji.Variable segment : eqType.Definition path := seq segment.(* amida-kuji has determinstic function to obtain next segment *)Variable next : segment -> option segment.Definition valid_path (seg : segment) (p : path) : bool := all id (pairmap (fun x y => next x =