fact: Fixpoint gtree_restrict t r {struct t} := match r, t with | GtrNil, _ => GtreePair GtreeEmpty t | _, GtreeNode t0 t1 t2 t3 => let cont r0 r1 r2 r3 := gtree_cons_pairs t (gtree_restrict t0 r0) (gtree_restrict t1 r1) (gtree_restrict t2 r2) (gtree_restrict t3 r3) in gtr_split cont GtrNil GtrNil GtrNil GtrNil r | _, GtreeLeaf0 => if gtr_match0 r then gtp_0_e else gtp_e_0 | _, GtreeLeaf1 => if gtr_match1 r then gtp_1_e else gtp_e_1 | _, GtreeLeaf2 => if gtr_match2 r then gtp_2_e else gtp_e_2 | _, GtreeLeaf3 => if gtr_match3 r then gtp_3_e else gtp_e_3 | _, GtreeLeaf01 => if gtr_match0 r then if gtr_match1 r then gtp_01_e else gtp_0_1 else if gtr_match1 r then gtp_1_0 else gtp_e_01 | _, GtreeLeaf12 => if gtr_match1 r then if gtr_match2 r then gtp_12_e else gtp_1_2 else if gtr_match2 r then gtp_2_1 else gtp_e_12 | _, GtreeLeaf13 => if gtr_match1 r then if gtr_match3 r then gtp_13_e else gtp_1_3 else if gtr_match3 r then gtp_3_1 else gtp_e_13 | _, GtreeLeaf23 => if gtr_match2 r then if gtr_match3 r then gtp_23_e else gtp_2_3 else if gtr_match3 r then gtp_3_2 else gtp_e_23 | _, GtreeEmpty => empty_gtree_pair end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree chromogram gtree)