proposition: Lemma methID_injective {n'} : forall (methSigs : Vector.t methSig n'), NoDup (Vector.to_list (Vector.map methID methSigs)) -> ListFacts1.IsInjection (fun midx => methID (Vector.nth methSigs midx)).
proof: Proof. unfold ListFacts1.IsInjection. intros. revert methSigs H H0. pattern n', x, y. eapply Fin.rect2; intros. - congruence. - revert f H H0. pattern n, methSigs. eapply Vector.caseS; simpl; intros. rewrite Vector_ToList_cons in H; inversion H; subst. generalize t H3; clear. induction f; simpl. + intro; pattern n, t; eapply Vector.caseS; intros. simpl in *. rewrite Vector_ToList_cons in H3. simpl in H3; intuition. + intro; revert f IHf; pattern n, t; eapply Vector.caseS; intros. simpl in *. rewrite Vector_ToList_cons in H3; simpl in H3. eapply IHf; intuition. - revert f H H0. pattern n, methSigs. eapply Vector.caseS; simpl; intros. rewrite Vector_ToList_cons in H; inversion H; subst. generalize t H3; clear. induction f; simpl. + intro; pattern n, t; eapply Vector.caseS; intros. simpl in *. rewrite Vector_ToList_cons in H3. simpl in H3; intuition. + intro; revert f IHf; pattern n, t; eapply Vector.caseS; intros. simpl in *. rewrite Vector_ToList_cons in H3; simpl in H3. eapply IHf; intuition. - revert f g H H0 H1; clear. pattern n, methSigs. eapply Vector.caseS; intros. simpl in *. eapply H. rewrite Vector_ToList_cons in H0; inversion H0; subst; eauto. congruence. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction