proposition: Lemma T2eqE a b n d a' b' n' d': (cons a b n d == cons a' b' n' d') = [&& a == a', b == b', n== n' & d == d' ].
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)