proposition: Lemma DecomposePrei3list_Agree av {numRepArgs} {A} {B} {C} {RepT' : Vector.t A numRepArgs} (RepT : ilist3 (B := B) RepT') (RepWrapper : @RepWrapperT av numRepArgs A B C RepT' RepT) : forall r' r, is_same_types (Vector.to_list (DecomposePrei3list (C := C) RepT' RepT RepWrapper r)) (Vector.to_list (DecomposePrei3list (C := C) RepT' RepT RepWrapper r')) = true.
proof: Proof. induction RepT'; simpl. - reflexivity. - intros. unfold Vector.to_list, is_same_types in *; simpl in *. apply IHRepT'. 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