fact: Definition bnode T (u v:order T) : order T := match tilt u v with i_eq => gnode u v | i_lt => match v with ostop t => gnode u v | onode a r s => match tilt r s with i_gt => match r with ostop q => gnode u v | onode b x y => gnode (gnode u x) (gnode y s) end | _ => gnode (gnode u r) s end end | i_gt => match u with ostop t => gnode u v | onode a r s => match tilt r s with i_lt => match s with ostop q => gnode u v | onode b x y => gnode (gnode r x) (gnode y v) end | _ => gnode r (gnode s v) end end end.