fact: Fixpoint Tristep' (r1 : Row) : Row -> Row -> Tri := fun r2 r3 => match r1 with | Nil => TrF r1 r2 r3 | C Keeper r1s => match r2, r3 with | C y r2s, C z r3s => match move (tri Keeper y z) with | CAN (tri x' y' z') => TrS (C x' r1s) (C y' r2s) (C z' r3s) | CANT => TrF r1 r2 r3 end | _, _ => TrF r1 r2 r3 end | C KeepOD r1s => match r2, r3 with | C y r2s, C z r3s => match move (tri KeepOD y z) with | CAN (tri x' y' z') => TrS (C x' r1s) (C y' r2s) (C z' r3s) | CANT => TrF r1 r2 r3 end | _, _ => TrF r1 r2 r3 end | C x r1s => match r2, r3 with | C y r2s, C z r3s => match Tristep' r1s r2s r3s with | TrS r1' r2' r3' => TrS (C x r1') (C y r2') (C z r3') | TrF r1' r2' r3' => TrF (C x r1') (C y r2') (C z r3') end | _, _ => TrF r1 r2 r3 end end.