proposition: Lemma compiled_prog_op_refines_ax av (env : StringMap.t DFFun -> Env av) {numRepArgs} {A} {B} {C} {RepSpec RepImpl} (AbsR : RepSpec -> RepImpl -> Prop) {RepT' : Vector.t A numRepArgs} (RepT : ilist3 (B := B) RepT') (RepMap : RepImpl -> i3list C RepT) (RepWrapper : @RepWrapperT av numRepArgs A B C RepT' RepT) (DecomposeRep := fun repWrapper rep => Decomposei3list RepT' RepT repWrapper (RepMap rep)) (DecomposeRepPre := fun rep => DecomposePrei3list RepT' RepT RepWrapper (RepMap rep)) (DecomposeRepPost := fun rep rep' => DecomposePosti3list _ RepT RepWrapper (RepMap rep) (RepMap rep')) (DecomposeRepPrePostAgree := fun r r' => DecomposePrei3list_Agree av RepT RepWrapper (RepMap r) (RepMap r')) cod dom codWrap domWrap methSpec methImpl (ValidMeth : refineMethod AbsR methSpec methImpl) RepInv progOK : forall env_ext, op_refines_ax (env env_ext) (Core (BuildDFFun env (cod := cod) (dom := dom) (WrappedCod := codWrap) (WrappedDom := domWrap) (meth := methImpl) (RepInv := RepInv) DecomposeRep numRepArgs RepWrapper progOK)) (GenAxiomaticSpecs (numRepArgs := numRepArgs) AbsR RepInv codWrap domWrap methSpec DecomposeRepPre DecomposeRepPost DecomposeRepPrePostAgree).
proof: Proof. unfold op_refines_ax; repeat split. - unfold GenAxiomaticSpecs; simpl. unfold AxiomatizeMethodPostSpec. eapply AxiomatizeMethodPostSpec_OK. - simpl. unfold BuildArgNames. rewrite app_length, !rev_length, !map_length, !NumUpTo_length; simpl. intros; destruct H as [r [r' [AbsR_r_r' [H' H ] ] ] ]. apply length_AxiomatizeMethodPre' in H; subst. rewrite <- H, length_Vector_to_list, <- !plus_n_O; auto with arith. - destruct progOK as [prog [op_spec ?] ]; simpl. generalize ValidMeth op_spec; clear. unfold AxSafe; simpl; intros. destruct_ex; intuition; subst. unfold AxiomatizeMethodPreSpec in H2; simpl in H2; destruct_ex; intuition; subst. revert st x x1 H0 H x0 H1 H2 H4 X0. replace (Datatypes.length dom) with (Datatypes.length (@nil (Value av)) + Datatypes.length (dom)). assert ( Datatypes.length (@nil (Value av)) = Datatypes.length (@nil {T : Type & (NameTag av T * Comp T)%type})) as len_l_l' by reflexivity. assert (forall x0, make_map (BuildArgNames (List.length (@nil (Value av))) numRepArgs) (nil ++ (Vector.to_list (DecomposeRepPre x0))) ≲ list2Telescope (nil ++ DecomposeRep RepWrapper x0) ∪ ∅) as H''. { unfold BuildArgNames. subst DecomposeRep; subst DecomposeRepPre; subst DecomposeRepPrePostAgree. simpl. clear methSpec methImpl ValidMeth op_spec RepInv. generalize RepT RepMap RepWrapper; clear; induction RepT'. - intros; simpl; reflexivity. - simpl; intros. rewrite NumUpTo_nil, map_app, rev_app_distr; simpl. rewrite Vector_ToList_cons. rewrite StringMapFacts.add_eq_o; eauto. eexists _; intuition eauto. eapply StringMap_remove_add; eauto. eapply (IHRepT' (prim_snd RepT) (fun rep => prim_snd (RepMap rep))). eapply make_map_not_in. rewrite <- in_rev, in_map_iff; intro; destruct_ex; intuition. injections. destruct x; destruct n. + intuition. + symmetry in H. apply NumberToString_rec_10 in H; intuition. + apply NumberToString_rec_10 in H; intuition. + apply NumberToString_rec_inj' in H; simpl in H; subst; eauto. simpl in H1. apply ListFacts4.in_nth_error in H1; destruct_ex. apply nth_error_NumUpTo_eq in H; simpl in H; intuition; subst. } remember (@nil (Value av)) as l; clear Heql. remember [] as l'; clear Heql'. remember DecomposeRep. assert (forall r, RepInv r -> LiftMethod' (env env_ext) dom RepInv (fun r0 => list2Telescope (DecomposeRep RepWrapper r0)) (l0 RepWrapper r) codWrap domWrap prog l' (methImpl r)) as op_spec' by (subst; exact (op_spec env_ext)); clear op_spec. clear Heql0. generalize l l' DecomposeRep DecomposeRepPre l0 op_spec' len_l_l' H''. clear methSpec ValidMeth l l' DecomposeRep DecomposeRepPre l0 op_spec' len_l_l' H''. induction dom; simpl; intros. + destruct cod; simpl. { simpl in *; subst. eapply op_spec'; eauto. eapply SameValues_Equal. symmetry; apply H. rewrite <- plus_n_O. apply H''. } { eapply op_spec'; eauto. simpl in *; subst. eapply SameValues_Equal. symmetry; apply H. rewrite <- plus_n_O. apply H''. } + simpl in *; destruct_ex; subst. rewrite H. destruct domWrap. eapply IHdom with (methImpl := fun r => methImpl r x2) (l' := (existT (fun T : Type => (NameTag av T * Comp T)%type) a (NTSome (String "a" (String "r" (String "g" (NumberToString_rec (Datatypes.length l') (pred (Datatypes.length l')))))), ret x2) :: l')) (DecomposeRepPre := DecomposeRepPre); auto. 7:apply H3. 6:eauto. 5:eauto. simpl; eauto. unfold BuildArgNames; simpl. rewrite NumUpTo_nil, map_app, rev_app_distr; simpl. intros; rewrite len_l_l'. rewrite StringMapFacts.add_eq_o; eauto. eexists; intuition eauto. eapply StringMap_remove_add; eauto. unfold BuildArgNames in H''. rewrite NumUpTo_nil, map_app, rev_app_distr, len_l_l' in H''; simpl in H''. eapply H''. eapply make_map_not_in. intro H'; apply in_app_or in H'; rewrite <- in_rev, in_map_iff in H'; intuition; destruct_ex; intuition. injections. destruct x4; destruct l'. * intuition. * symmetry in H4. apply NumberToString_rec_10 in H4; intuition. simpl; omega. * apply NumberToString_rec_10 in H4; intuition. * apply NumberToString_rec_inj' in H4; simpl in H4; subst; eauto. simpl in H6. apply ListFacts4.in_nth_error in H6; destruct_ex. apply nth_error_NumUpTo_eq in H4; simpl in H4; intuition; subst. * rewrite <- in_rev, in_map_iff in H4; destruct_ex. unfold nthRepName in H4; simpl in H4; intuition. discriminate. * simpl; rewrite H0; repeat f_equal; omega. * simpl; f_equiv; f_equal; omega. + reflexivity. - destruct progOK as [prog [op_spec ?] ]; simpl. generalize ValidMeth op_spec; clear. unfold AxSafe, AxRunsTo; simpl; intros. unfold AxiomatizeMethodPreSpec in *. destruct_ex; intuition; subst. destruct_ex; intuition; subst. revert st x x0 H1 H0 H H1 H2 H5 H3 x. replace (Datatypes.length dom) with (Datatypes.length (@nil (Value av)) + Datatypes.length (dom)). assert ( Datatypes.length (@nil (Value av)) = Datatypes.length (@nil {T : Type & (NameTag av T * Comp T)%type})) as len_l_l' by reflexivity. assert (forall x0, make_map (BuildArgNames (List.length (@nil (Value av))) numRepArgs) (nil ++ (Vector.to_list (DecomposeRepPre x0))) ≲ list2Telescope (nil ++ DecomposeRep RepWrapper x0) ∪ ∅) as H''. { unfold BuildArgNames. subst DecomposeRep; subst DecomposeRepPre. simpl. clear methSpec methImpl ValidMeth op_spec RepInv. generalize RepT RepMap RepWrapper; clear; induction RepT'; simpl; intros. - reflexivity. - rewrite NumUpTo_nil, map_app, rev_app_distr; simpl. rewrite Vector_ToList_cons. rewrite StringMapFacts.add_eq_o; eauto. eexists _; intuition eauto. eapply StringMap_remove_add; eauto. eapply (IHRepT' (prim_snd RepT) (fun rep => prim_snd (RepMap rep))). eapply make_map_not_in. rewrite <- in_rev, in_map_iff; intro; destruct_ex; intuition. injections. destruct x; destruct n. + intuition. + symmetry in H. apply NumberToString_rec_10 in H; intuition. + apply NumberToString_rec_10 in H; intuition. + apply NumberToString_rec_inj' in H; simpl in H; subst; eauto. simpl in H1. apply ListFacts4.in_nth_error in H1; destruct_ex. apply nth_error_NumUpTo_eq in H; simpl in H; intuition; subst. } unfold AxiomatizeMethodPostSpec. remember (@nil (Value av)) as l; clear Heql. remember (@nil {T : Type & (NameTag av T * Comp T)%type}) as l'. remember DecomposeRep. assert (forall r, RepInv r -> LiftMethod' (env env_ext) dom RepInv (fun r0 => list2Telescope (DecomposeRep RepWrapper r0)) (l0 RepWrapper r) codWrap domWrap prog l' (methImpl r)) as op_spec' by (subst; exact (op_spec env_ext)); clear op_spec. replace (@nil (prod (Value av) (option av))) with (map (fun v : Value av => (v, @None av)) l) by (subst; destruct l; simpl in *; congruence). clear Heql'; clear Heql0. intros st x x0. generalize ValidMeth l l' l0 st x x0 op_spec' len_l_l' H''. clear l l' l0 st x x0 op_spec' len_l_l' H''. induction dom; simpl; intros. + destruct cod. { apply op_spec' in H3; destruct H3. destruct (H3 _ (H'' _)). rewrite H in H0; subst. rewrite <- plus_n_O in H0; apply H8 in H0. simpl in methSpec, methImpl. destruct H0; intuition; destruct x. repeat eexists _; intuition eauto. repeat (eexists _); intuition eauto. pose proof (ValidMeth _ _ H4 _ H5); computes_to_inv. destruct v; simpl in *. injections. repeat (eexists _); intuition eauto. unfold BuildArgNames. rewrite <- plus_n_O in *. unfold DecomposeRepPost. revert H9; case_eq (StringMap.find "ret" st'); try tauto; intros. destruct_ex; intuition; computes_to_inv; subst. rewrite !combine_app_distrib, map_app, combine_app_distrib. f_equal. unfold DecomposeRep in H13. apply StringMap.find_2 in H9. simpl in H13. generalize (SameValues_PushExt (fun _ => list2Telescope (Decomposei3list RepT' RepT RepWrapper (RepMap r))) _ _ H9 H13); clear. - induction l; simpl; eauto. rewrite NumUpTo_nil, map_app, rev_app_distr; simpl. intros; rewrite IHl; f_equal; eauto. destruct a; eauto. case_eq (StringMap.find (elt:=Value av) (String "a" (String "r" (String "g" (NumberToString_rec (Datatypes.length l) (pred (Datatypes.length l)))))) st'); intros; eauto. destruct v; eauto. exfalso; generalize st' H0 H; clear. induction RepT'. + simpl; intros; unfold WeakEq in *; intuition. unfold SameADTs in H0. apply StringMap.find_2 in H0. apply H1 in H0. apply StringMap.add_3 in H0; try congruence. apply StringMap.is_empty_2 in H0; eauto. + intros. simpl in H; unfold nthRepName in H. simpl in H. destruct (StringMap.find (elt:=Value av) (String "r" (String "e" (String "p" (NumberToString_rec n (pred n))))) st'); eauto. destruct_ex; intuition. eapply (IHRepT' (prim_snd RepT) (fun rep => prim_snd (RepMap rep))). 2: eauto. apply StringMap.find_1; apply StringMap.remove_2; eauto using StringMap.find_2. - apply StringMap.find_2 in H9. generalize st' (SameValues_PushExt (fun _ => list2Telescope (Decomposei3list RepT' RepT RepWrapper (RepMap r))) _ _ H9 H13); clear. induction RepT'. + reflexivity. + simpl. destruct RepWrapper; simpl in *. rewrite Vector_ToList_cons. intro; caseEq (StringMap.find (elt:=Value av) (String "r" (String "e" (String "p" (NumberToString_rec n (pred n))))) st'); intros; eauto. unfold DecomposeRepPre; simpl. rewrite NumUpTo_nil, map_app, rev_app_distr; simpl. rewrite Vector_ToList_cons. destruct_ex; split_and; subst. computes_to_inv; subst. simpl; rewrite H. f_equal. idtac. erewrite <- (IHRepT' (prim_snd RepT) (fun rep => prim_snd (RepMap rep))). 2:apply H3. f_equal. destruct (RepMap x1); destruct RepT; simpl in *. intros; eapply in_map; clear; intros. unfold get_output; destruct a; simpl. destruct v; eauto. rewrite remove_neq_o; eauto. revert H; clear. intros. apply in_combine_l in H. apply In_rev in H; eapply in_map_iff in H; destruct_ex; intuition; subst; simpl in H1; injections. apply ListFacts4.in_nth_error in H2; destruct_ex; apply nth_error_NumUpTo_eq in H0; intuition. destruct x; destruct n; try omega. symmetry in H. apply NumberToString_rec_10 in H; intuition. apply NumberToString_rec_inj' in H; simpl in H; omega. intuition. - rewrite map_length. rewrite (fun H => proj1 (lenth_combine _ _ H)). rewrite rev_length, map_length, NumUpTo_length; simpl; omega. rewrite rev_length, map_length, NumUpTo_length; simpl; omega. - rewrite rev_length, map_length, NumUpTo_length; simpl; omega. - simpl in H7. pose proof (ValidMeth _ _ H4 _ H5); computes_to_inv; subst. simpl in H9. revert H9; caseEq (StringMap.find (elt:=Value av) "ret" st'); intros; destruct_ex; intuition; subst. computes_to_inv; subst; auto. - unfold no_adt_leak; intros. unfold sel in H0. simpl in H7. destruct (string_dec "ret" var). intuition. rewrite <- remove_neq_o with (x := "ret") in H0; auto. right. simpl in H9. revert H9; caseEq (StringMap.find (elt:=Value av) "ret" st'); try tauto. destruct_ex; intuition; subst. generalize st' H0 H13 n. clear; induction l; simpl. + induction RepT'; simpl. * intros; destruct H13. unfold SameADTs in H. rewrite <- find_mapsto_iff in H0. rewrite <- H in H0. apply StringMap.empty_1 in H0; intuition. * intros; destruct (string_dec var ("rep" ++ (NumberToString_rec n (pred n)))); subst. { simpl in *. rewrite H0 in H13; destruct_ex; intuition; subst. computes_to_inv; subst. exists 0; eexists _; split; eauto; simpl. rewrite NumUpTo_nil, map_app, rev_app_distr; simpl; eauto. unfold DecomposeRepPre; simpl; rewrite Vector_ToList_cons; eauto. } destruct (StringMap.find (String "r" (String "e" (String "p" (NumberToString_rec n (pred n))))) (StringMap.remove (elt:=Value av) "ret" st')); try tauto. destruct_ex; intuition; computes_to_inv; subst. rewrite SameValues_remove2 in H3. eapply (IHRepT' (prim_snd RepT) (fun rep => prim_snd (RepMap rep))) in H3; eauto. repeat destruct_ex; intuition. unfold BuildArgNames in H1; simpl in H1. eexists (S x); exists x0; split. rewrite NumUpTo_nil, map_app, rev_app_distr; simpl; eauto. unfold DecomposeRepPre; simpl; rewrite Vector_ToList_cons; eauto. repeat rewrite remove_o in *; repeat find_if_inside; try discriminate. simpl in *; rewrite e in n1; congruence. eauto. + intros. destruct (IHl st') as [i' [ai' [? ? ] ] ]; eauto; eexists (S i'); simpl. eexists ai'. unfold BuildArgNames; simpl; rewrite NumUpTo_nil, map_app, rev_app_distr; simpl; eauto. } { apply op_spec' in H3; destruct H3. destruct (H3 _ (H'' _)). rewrite H in H0; subst. rewrite <- plus_n_O in H0; apply H8 in H0. simpl in *. simpl in H0. destruct H0; intuition. repeat eexists _; intuition eauto. repeat eexists _; intuition eauto. pose proof (ValidMeth _ _ H4 _ H5); computes_to_inv; subst. repeat (eexists _); intuition eauto. unfold BuildArgNames. rewrite <- plus_n_O in *. unfold DecomposeRepPost. revert H9; case_eq (StringMap.find (elt:=Value av) "ret" st'); intros; try tauto. destruct_ex; intuition; computes_to_inv; subst. rewrite !combine_app_distrib, map_app, combine_app_distrib. f_equal. unfold DecomposeRep in H13. apply StringMap.find_2 in H9. generalize st' (SameValues_PushExt (fun _ => list2Telescope (Decomposei3list RepT' RepT RepWrapper (RepMap x))) _ _ H9 H13); clear. - induction l; simpl; eauto. rewrite NumUpTo_nil, map_app, rev_app_distr; simpl. intros; rewrite IHl; f_equal; eauto. destruct a; eauto. case_eq (StringMap.find (elt:=Value av) (String "a" (String "r" (String "g" (NumberToString_rec (Datatypes.length l) (pred (Datatypes.length l)))))) st'); intros; eauto. destruct v; eauto. apply StringMap.find_2 in H0. apply (StringMap.remove_2 (x := "ret")) in H0; try congruence. apply StringMap.find_1 in H0. exfalso; generalize st' H0 H; clear. induction RepT'. + simpl; intros; unfold WeakEq in *; intuition. unfold SameADTs in H1. apply StringMap.find_2 in H0. rewrite StringMapFacts.remove_mapsto_iff in H0; intuition. apply H1 in H3. rewrite StringMapFacts.add_mapsto_iff in H3; intuition try congruence. apply StringMap.is_empty_2 in H4; eauto. + intros. simpl in H. destruct (StringMap.find (elt:=Value av) (String "r" (String "e" (String "p" (NumberToString_rec n (pred n))))) st' ); eauto. destruct_ex; intuition. eapply (IHRepT' (prim_snd RepT) (fun rep => prim_snd (RepMap rep))). 2: eassumption. rewrite SameValues_remove2. apply StringMap.find_1; apply StringMap.remove_2; eauto using StringMap.find_2. - generalize st' H13; clear. induction RepT'. + reflexivity. + unfold DecomposeRep. simpl. destruct RepWrapper; simpl in *. rewrite Vector_ToList_cons. intro; caseEq (StringMap.find (elt:=Value av) (String "r" (String "e" (String "p" (NumberToString_rec n (pred n))))) (StringMap.remove (elt:=Value av) "ret" st')); intros; eauto. unfold DecomposeRepPre; simpl. rewrite NumUpTo_nil, map_app, rev_app_distr; simpl. rewrite Vector_ToList_cons. destruct_ex; split_and; subst. computes_to_inv; subst. rewrite remove_neq_o in H; try congruence. simpl; rewrite H. f_equal. rewrite SameValues_remove2 in H3. erewrite <- (IHRepT' (prim_snd RepT) (fun rep => prim_snd (RepMap rep))). 2:apply H3. f_equal. destruct (RepMap x); destruct RepT; simpl in *. intros; eapply in_map; clear; intros. unfold get_output; destruct a; simpl. destruct v; eauto. rewrite remove_neq_o; eauto. revert H; clear. intros. apply in_combine_l in H. apply In_rev in H; eapply in_map_iff in H; destruct_ex; intuition; subst; simpl in H1; injections. apply ListFacts4.in_nth_error in H2; destruct_ex; apply nth_error_NumUpTo_eq in H0; intuition. destruct x; destruct n; try omega. symmetry in H. apply NumberToString_rec_10 in H; intuition. apply NumberToString_rec_inj' in H; simpl in H; omega. intuition. - rewrite map_length. rewrite (fun H => proj1 (lenth_combine _ _ H)). rewrite rev_length, map_length, NumUpTo_length; simpl; omega. rewrite rev_length, map_length, NumUpTo_length; simpl; omega. - rewrite rev_length, map_length, NumUpTo_length; simpl; omega. - simpl in H9. revert H9; caseEq (StringMap.find (elt:=Value av) "ret" st'); intros; destruct_ex; intuition; subst. computes_to_inv; subst; auto. - unfold no_adt_leak; intros. unfold sel in H0. simpl in H9. destruct (string_dec "ret" var). intuition. rewrite <- remove_neq_o with (x := "ret") in H0; auto. right. revert H9; caseEq (StringMap.find (elt:=Value av) "ret" st'); try tauto. destruct_ex; intuition; subst. generalize st' H0 H13 n. clear; induction l; simpl. + induction RepT'; simpl. * intros; destruct H13. unfold SameADTs in H. rewrite <- find_mapsto_iff in H0. rewrite <- H in H0. apply StringMap.empty_1 in H0; intuition. * intros; destruct (string_dec var ("rep" ++ (NumberToString_rec n (pred n)))); subst. { simpl in *. rewrite H0 in H13; destruct_ex; intuition; subst. computes_to_inv; subst. exists 0; eexists _; split; eauto; simpl. rewrite NumUpTo_nil, map_app, rev_app_distr; simpl; eauto. unfold DecomposeRepPre; simpl; rewrite Vector_ToList_cons; eauto. } destruct (StringMap.find (String "r" (String "e" (String "p" (NumberToString_rec n (pred n))))) (StringMap.remove (elt:=Value av) "ret" st')); try tauto. destruct_ex; intuition; computes_to_inv; subst. rewrite SameValues_remove2 in H3. eapply (IHRepT' (prim_snd RepT) (fun rep => prim_snd (RepMap rep))) in H3; eauto. repeat destruct_ex; intuition. unfold BuildArgNames in H1; simpl in H1. eexists (S x0); exists x2; split. rewrite NumUpTo_nil, map_app, rev_app_distr; simpl; eauto. unfold DecomposeRepPre; simpl; rewrite Vector_ToList_cons; eauto. repeat rewrite remove_o in *; repeat find_if_inside; try discriminate. simpl in *; rewrite e in n1; congruence. eauto. + intros. destruct (IHl st') as [i' [ai' [? ? ] ] ]; eauto; eexists (S i'); simpl. eexists ai'. unfold BuildArgNames; simpl; rewrite NumUpTo_nil, map_app, rev_app_distr; simpl; eauto. } + repeat destruct_ex; intuition. setoid_rewrite H. destruct domWrap. rewrite Plus.plus_comm. simpl. simpl in ValidMeth. destruct (IHdom d (fun r => methSpec r x3) (fun r => methImpl r x3) (fun r_o r_n AbsR' => ValidMeth r_o r_n AbsR' x3) (fun r_o r_n AbsR' => ValidMeth r_o r_n AbsR' x3) ((wrap (FacadeWrapper := gWrap g) x3) :: l) ((existT (fun T : Type => (NameTag av T * Comp T)%type) a (@NTSome _ _ (String "a" (String "r" (String "g" (NumberToString_rec (Datatypes.length l') (pred (Datatypes.length l')))))) (gWrap g), ret x3)) :: l') l0 st x x0); simpl; auto. intros; unfold BuildArgNames. rewrite NumUpTo_nil, map_app, rev_app_distr; simpl; eauto. rewrite NumUpTo_nil, map_app, rev_app_distr; simpl; eauto. rewrite len_l_l'. rewrite add_eq_o by eauto. pose proof (op_spec' _ H3 x3). eexists; intuition eauto. eapply StringMap_remove_add; eauto. unfold BuildArgNames in H''. rewrite <- len_l_l'; eauto. eapply make_map_not_in. intro; apply in_app_or in H7; intuition. rewrite <- in_rev, in_map_iff in H8; destruct_ex; intuition. simpl in H8. injections. destruct x5; destruct (Datatypes.length l'). * intuition. * symmetry in H7. apply NumberToString_rec_10 in H7; intuition. * apply NumberToString_rec_10 in H7; intuition. * apply NumberToString_rec_inj' in H7; simpl in H7; subst; eauto. apply ListFacts4.in_nth_error in H9; destruct_ex. apply nth_error_NumUpTo_eq in H7; simpl in H7; intuition; subst. * rewrite <- in_rev, in_map_iff in H8; destruct_ex; intuition. simpl in H8; discriminate. * rewrite H1; f_equal; f_equal; omega. * rewrite Plus.plus_comm in H; simpl in H; rewrite Plus.plus_comm in H; eauto. * rewrite Plus.plus_comm in H1; simpl in H1; rewrite Plus.plus_comm in H1; eauto. * destruct_ex; intuition; eexists x4; exists x5; intuition eauto. simpl in H5; rewrite Plus.plus_comm; eauto. simpl in H4; rewrite Plus.plus_comm; eauto. rewrite Plus.plus_comm in H. rewrite <- H6, H. rewrite Plus.plus_comm; simpl; reflexivity. destruct_ex; simpl in H6. eexists x6; eexists x7; intuition. exists x3. rewrite Plus.plus_comm. apply H12. simpl in H9; rewrite Plus.plus_comm; eauto. + reflexivity. 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