proposition: Lemma IsInjection_nthArgName : ListFacts1.IsInjection nthArgName.
proof: Proof. unfold ListFacts1.IsInjection. unfold nthArgName, not; intros. apply H. injections. destruct x; destruct y; simpl. + congruence. + exfalso. symmetry in H1; apply (fun H H' => NumberToString_rec_10 _ _ H H' H1); auto with arith. + exfalso. apply (fun H H' => NumberToString_rec_10 _ _ H H' H1); auto with arith. + rewrite (@NumberToString_rec_inj' (S x) x y (S y)); auto with arith. 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