fact: Definition gtree_merge_pairs pt0 pt1 pt2 := let: GtreePair t0 t0' := pt0 in let: GtreePair t1 t1' := pt1 in let: GtreePair t2 t3 := pt2 in GtreePair (GtreeNode t0 t1' t2 t3) (GtreeNode t0' t1 t3 t2).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree dyck)