proposition: Lemma GoodWrapperConsistent {av A} (gWrapper : GoodWrapper av A) : forall a1 a2: A, is_same_type (@wrap _ _ (gWrap gWrapper) a1) (@wrap _ _ (gWrap gWrapper) a2).
proof: Proof. intros. unfold is_same_type. pose proof (gWrapTagConsistent gWrapper). find_if_inside; destruct (H a1); destruct (H a2); rewrite H0, H1; eauto. 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