fact: Fixpoint gtree_init_table d h' {struct h'} : gtree_table := if h' is h''.+1 then let tab := gtree_init_table d.+1 h'' in if tab is [:: pt1, pt0 & lpt] then gtree_merge_line pt0 pt1 empty_gtree_pair lpt d else tab else init_gtree_h1.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree dyck)