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