fact: Fixpoint stepnorth (b : Board) : Board := match b with | R l1 (R l2 (K l3 b')) => match Tristep' l3 l2 l1 with | TrS l3' l2' l1' => R l1' (K l2' (R l3' b')) | TrF l3' l2' l1' => R l1' (R l2' (K l3' b')) end | R r b' => R r (stepnorth b') | _ => b end.