fact: Fixpoint vector_dec {n} (a : vector T n) : forall b : vector T n, {a = b} + {a <> b} := match a in vector _ n return forall b : vector T n, {a = b} + {a <> b} with | Vnil => fun b => left match b in vector _ 0 with | Vnil => eq_refl end | Vcons _ a a' => fun b => match b as b in vector _ (S n) return forall a', (forall a : vector T n, {a' = a} + {a' <> a}) -> {Vcons a a' = b} + {Vcons a a' <> b} with | Vcons _ b b' => fun a' rec => match Tdec a b , rec b' with | left pf , left pf' => left match pf , pf' with | eq_refl , eq_refl => eq_refl end | right pf , _ => right (fun x : Vcons a a' = Vcons b b' => pf match x in _ = z return a = vector_hd z with | eq_refl => eq_refl end) | left _ , right pf => right (fun x : Vcons a a' = Vcons b b' => pf match x in _ = z return a' = vector_tl z with | eq_refl => eq_refl end) end end a' (@vector_dec _ a') end.
imports: ExtLib.Data.Fin