fact: Definition eqb: forall {m n} (v1: t A m) (v2: t A n), bool := fix fix_beq {m n} v1 v2 := match v1, v2 with |[], [] => true |_ :: _, [] |[], _ :: _ => false |h1 :: t1, h2 :: t2 => A_beq h1 h2 && fix_beq t1 t2 end%bool.
imports: VectorDef VectorSpec