proposition: Lemma GenAxiomaticSpecs_type_conforming av {Dom} {RepSpec RepImpl} (AbsR : RepSpec -> RepImpl -> Prop) (RepInv : RepImpl -> Prop) (dWrap : DomWrapperT av Dom) {numRepArgs : nat} (DecomposeRepPre : RepImpl -> Vector.t (Value av) numRepArgs) (_ : forall x x0, is_same_types (Vector.to_list (DecomposeRepPre x0)) (Vector.to_list (DecomposeRepPre x)) = true) : type_conforming (AxiomatizeMethodPreSpec AbsR RepInv DecomposeRepPre dWrap).
proof: Proof. unfold type_conforming. unfold AxiomatizeMethodPreSpec in *. remember nil; remember l. assert (is_same_types l0 l = true) by (rewrite <- Heql0, Heql; reflexivity). intros; rewrite Heql0 in H2. generalize dependent DecomposeRepPre. generalize dependent Rep. generalize numRepArgs. generalize l l0 H3 H0; clear. induction Dom; simpl; repeat cleanup. - unfold is_same_types in H0. revert H0 H H3; clear. revert l0. induction l; destruct l0; simpl in *; intros; try discriminate. + eauto. + apply Bool.andb_true_iff in H0; intuition. unfold is_same_types in *; simpl; rewrite H1; simpl. eapply IHl; eauto. - destruct dWrap. eapply IHDom with (l := wrap (FacadeWrapper := gWrap g) x1 :: l) (l0 := wrap (FacadeWrapper := gWrap g) x4 :: l0); eauto. unfold is_same_types in *. simpl; rewrite H0. rewrite GoodWrapperConsistent; simpl; 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