proposition: Lemma index_SumType_inj_inverse {n} : forall (tag : Fin.t n) (v : Vector.t Type n) (el : Vector.nth v tag), SumType_index v (inj_SumType v tag el) = tag.
proof: Proof. induction tag. - intro; pattern n, v; eapply Vector.caseS; simpl. clear; intros; destruct t; eauto. - intro; revert tag IHtag; pattern n, v; eapply Vector.caseS; simpl; intros. destruct t. + inversion tag. + f_equal. eapply IHtag. Qed.
imports: Coq.Vectors.Vector Coq.Vectors.Vector Fiat.Common.BoundedLookup