proposition: Lemma inj_SumType_proj_inverse {n} : forall (v : Vector.t Type n) (el : SumType v), inj_SumType v _ (SumType_proj v el) = el.
proof: Proof. induction v; simpl; intros. - destruct el. - destruct v. + simpl; reflexivity. + destruct el; simpl; eauto. f_equal; apply IHv. Qed.
imports: Coq.Vectors.Vector Coq.Vectors.Vector Fiat.Common.BoundedLookup