fact: Fixpoint T1eq x y {struct x} := match x, y with | zero, zero => true | cons a n b, cons a' n' b' => [&& T1eq a a', n== n' & T1eq b b' ] | _, _ => false end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)