Library iris.program_logic.refine_raw_adequacy

From iris.program_logic Require Import wsat ownership.
From iris.program_logic Require Import adequacy.
From iris.program_logic Require Export ghost_ownership refine_raw.
From iris.prelude Require Export set irelations natmap mapset.
From iris.algebra Require Import dra cmra_tactics.
From iris.program_logic Require Import language wsat adequacy_inf.
Ltac solve_included' A :=
  ra_reflection.quote;
  eapply (@ra_reflection.flatten_correct A), (bool_decide_unpack _);
  vm_compute; apply I.

Ltac solve_equiv':=
  match goal with
    | |- ?x ?y
    let A := match type of y with | ucmra_car ?A'A' | ?A'A' end in
    ra_reflection.quote;
      eapply (@ra_reflection.flatten_correct_equiv A), (bool_decide_unpack _);
      vm_compute; apply I
  end.

Ltac solve_validN' :=
  match goal with
  | H : ✓{?n} ?y |- ✓{?n'} ?x
    let A := match type of y with | ucmra_car ?A'A' | ?A'A' end in
     let Hn := fresh in let Hx := fresh in
     assert (n' n) as Hn by omega;
     assert (x y) as Hx by solve_included' A;
     eapply cmra_validN_le, Hn; eapply cmra_validN_included, Hx; apply H
  end.

Ltac solve_valid' :=
  match goal with
  | H : ?y |- ?x
    let A := match type of y with | ucmra_car ?A'A' | ?A'A' end in
     let Hn := fresh in let Hx := fresh in
     assert (x y) as Hx by solve_included' A;
     eapply cmra_valid_included, Hx; apply H
  end.

Lemma elem_of_In {A: Type}: (l: list A) a, a l In a l.
Proof.
  induction l as [| a' l]; first set_solver.
  split.
  - intros [->| Hin]%elem_of_cons.
    × left. auto.
    × right. eapply IHl; eauto.
  - simpl. intros [->|Hin].
    × left.
    × right. eapply IHl; eauto.
Qed.

Local Hint Extern 10 ( _) ⇒
  repeat match goal with
  | H : wsat _ _ _ _ _ |- _apply wsat_valid in H; last omega
  end; first [ solve_valid || solve_valid' ].
Local Hint Extern 10 (✓{_} _) ⇒
  repeat match goal with
  | H : wsat _ _ _ _ _ |- _apply wsat_valid in H; last omega
  end; first [ solve_valid || solve_validN' ].

Definition alt_triv Λ Σ (g: gid Σ) :=
   (gid': gid Σ) A, gid' g A = projT2 Σ gid' (iPreProp Λ (globalF Σ))
                      trivial_step A.

Class refineG (Λ : language) (Σ : gFunctors) (: language) (K: nat) := {
  refine_inG :> inG Λ Σ (refine_ucmra K);
  refine_Knz : K 0;
  refine_alt_triv: alt_triv Λ Σ (@inG_id _ _ _ refine_inG)
}.

Definition refineGF K : gFunctor := GFunctor (constURF (refine_ucmra K)).
Instance inGF_refineG `{Hin: inGF Λ Σ (refineGF K)} `{HK_nz: K 0}
         (Htriv: alt_triv Λ Σ (@inGF_id _ _ _ Hin)) : refineG Λ Σ K.
Proof. refine {| refine_inG := inGF_inG_transparent Hin |}; auto. Qed.

Section refine_raw_adequacy.
Context (: language).
Context (K: nat).
Context (K_nz: K 0).

  Notation refine_cmra K := (validity (refineDR K)).
Definition refine v ts cs ixs : refine_cmra K :=
  to_validity (Refine K v ts cs ixs).
  Context `{is_in: refineG Λ Σ K}.

  Definition trivial_step (A: cmraT) :=
     (a a': A) n, a _(n) a'.

  Definition master_own (c: cfg ) :=
    ( cfg0 idx0, owne (refine master (cfg0 ++ [c]) idx0))%I.
  Definition master_own_exact (cs: list (cfg )) idxs :=
    owne (refine master cs idxs)%I.
  From iris.algebra Require Import upred.

  Definition snapshot_ownl tids (c: cfg ) :=
    ( cfg0 idx0, ownle (refine snapshot tids (cfg0 ++ [c]) idx0))%I.
  Definition snapshot_ownl_exact tids cs idxs :=
    ownle (refine snapshot tids cs idxs)%I.

  Lemma init_own_snap_master_valid E σ:
     ((to_globalFe (refine snapshot {[0]} ([([E], σ)]) []))
          (to_globalFe (refine master ([([E], σ)]) []))).
  Proof.
    rewrite /to_globalFe. intro i.
    case (@decide (i = (@inG_id Λ Σ _ (refine_inG))) (fin_dec _ _)).
    - intros →. rewrite iprod_lookup_op.
      rewrite ?iprod_lookup_singleton. rewrite -ucmra_transport_op.
      rewrite ucmra_transport_valid.
      split_and!; try econstructor; eauto.
      simpl. set_unfold. intros; omega.
      simpl. econstructor.
      simpl. set_solver+.
      econstructor.
      rewrite /refine. simpl.
      rewrite -{2}(app_nil_r ([]: list nat)).
      rewrite -{2}(app_nil_r [([E], σ)]).
      econstructor. set_solver+.
      set_solver+.
    - intros Hneq. rewrite iprod_lookup_op.
      rewrite ?iprod_lookup_singleton_ne; auto.
      rewrite ?right_id. apply ucmra_unit_valid.
  Qed.

  Definition interp_extract (r: iRes Λ (globalF Σ)) : refine_cmra K :=
    ucmra_transport (eq_sym inG_prf) ((gst r) (inG_id _)).


  Existing Instances validity_equiv refine_equiv validity_equivalence.

  Instance interp_extract_proper:
    Proper ((≡) ==> (≡)) interp_extract.
  Proof.
    rewrite /interp_extract. intros x y Heq.
    inversion Heq as [_ _ Heq'].
    rewrite (Heq' (inG_id _)) //.
  Qed.

        Lemma own_value_stopped P V ES sσ' k:
               nth_error ES k = Some (of_val V)
                (snapshot_ownl {[k]} (ES, sσ') P) uPred_stopped.
        Proof.
        intros Hnth.
        econstructor. rewrite /snapshot_ownl.
        uPred.unseal. intros n x y Hvalx Hvaly (?&?&?&?&Heqx&Heqy&Hsat&Haff).
        destruct Hsat as (cfgs&idxs&Hsat).
        rewrite ownle_eq /ownle_def in Hsat. simpl in Hsat. rewrite ownGl_spec in Hsat ×.
        intros Hequiv. rewrite Heqx Heqy. destruct Haff as (?&Haff).
        rewrite Haff ?right_id.
        rewrite -Hequiv.
        simpl.
        rewrite /uPred_holds.
        intros n' Hle. intro Hfalse.
        simpl in Hfalse.
        inversion Hfalse as [r' Hstep].
        simpl in Hstep. rewrite /stepN /cmra_stepN //= /res_stepN //= in Hstep ×.
        specialize (Hstep (@inG_id Λ Σ _ (refine_inG))).
        rewrite /to_globalFe //= in Hstep.
        rewrite iprod_lookup_singleton in Hstep.
        eapply ucmra_transport_stepN_adj in Hstep.
        inversion Hstep as [Hcov Hstep_car].
        rewrite Heqy Haff ?right_id in Hvaly *=>Hvaly.

        assert (Hcar_valid : refine snapshot {[k]} (cfgs ++ [(ES, sσ')])
                               idxs).
        {
          rewrite -Hequiv in Hvaly ×.
          intros Hval. destruct Hval as (_&_&Hval_gst).
          simpl in Hval_gst. unfold to_globalFe in Hval_gst.
          specialize (Hval_gst (@inG_id Λ Σ _ (refine_inG))).
          rewrite iprod_lookup_singleton in Hval_gst.
          rewrite ucmra_transport_validN in Hval_gst ×.
          auto.
        }
        
        specialize (Hstep_car Hcar_valid).
        simpl in Hstep_car.
        eapply refine_step_inv in Hstep_car
          as (cs0&c&c'&cspec&csext&i'&ispec&isext&Heqcs1&_&_&_
              &_&_&Hin_ext&_&Hval_step).
        simpl in ×.
        apply app_inj_2 in Heqcs1 as (Heqcfgs1&Heqc); auto.
        inversion Heqc as [Heqc'].
        rewrite -Heqc' in Hval_step.
        assert (i' = k). specialize (Hin_ext i'). set_unfold.
        eapply Hin_ext. auto.
        subst.
        clear -Hval_step Hnth.
        specialize (valid_cfg_extract'
                                       (ES, sσ')
                                       (cspec ++ csext)
                                       c'
                                       (ispec ++ isext ++ [k])).
        simpl. rewrite -app_assoc. intros Hextract.
        eapply Hextract in Hval_step. clear Hextract.
        rewrite app_assoc in Hval_step.
        remember (ispec ++ isext) as idxs eqn:Hidxs.
        clear Hidxs. revert ES sσ' c' Hval_step Hnth.
        induction idxs as [| i idxs].
        × simpl. intros. apply isteps_once in Hval_step.
           inversion Hval_step.
           subst. inversion H.
           subst. rewrite nth_error_app2 in Hnth; auto.
           replace (length t1 - length t1) with 0 in Hnth; last by omega.
           simpl in ×. inversion Hnth.
           subst.
           eapply val_stuck in H1.
           rewrite to_of_val in H1.
           congruence.
        × intros. simpl in ×.
          inversion Hval_step as [| ? ? ? y ? Hstep Histeps] . subst.
           case (decide (i = k)).
           ** intros. subst.
             inversion Hstep.
             inversion H. subst.
             rewrite nth_error_app2 in Hnth.
           replace (length t1 - length t1) with 0 in Hnth; last by omega.
           simpl in ×. inversion Hnth.
           subst.
           eapply val_stuck in H1.
           rewrite to_of_val in H1.
           congruence. auto.
           ** intros.
               subst.
               destruct y.
               eapply IHidxs. eauto.
               eapply idx_step_diff in Hstep; eauto.
        Qed.

Context (PrimDet: (e: expr ) σ e1' σ1' ef1' e2' σ2' ef2',
            prim_step e σ e1' σ1' ef1'
            prim_step e σ e2' σ2' ef2'
            e1' = e2' σ1' = σ2' ef1' = ef2').

Context (PrimDec: (e: expr ) σ, { t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
                                    {¬ e' σ' ef', prim_step e σ e' σ' ef'}).

Instance PrimDecWeak (e: expr ) σ: Decision ( e' σ' ef', prim_step e σ e' σ' ef').
Proof.
  edestruct PrimDec as [(((e'&σ')&ef')&Hs)|].
  - left. e', σ', ef'. eauto.
  - right. eauto.
Qed.

Lemma idx_step_dec' (c: cfg ) (i: nat): { c' | idx_step i c c'} + {¬ c', idx_step i c c'}.
Proof.
  revert i.
  destruct c as (es&σ).
  induction es as [| e es].
  - right. intro Hf. destruct Hf as (c'&Hs). inversion Hs. subst. destruct t1;
      simpl in *; congruence.
  - destruct i.
    ** destruct (PrimDec e σ) as [(((e'&σ')&ef')&Hs)|Hfalse].
       *** econstructor.
            (e' :: es ++ option_list ef', σ').
           rewrite idx_step_equiv; econstructor; eauto.
       *** right. intros (c'&Hf). rewrite idx_step_equiv in Hf ×. inversion 1.
           subst. eapply Hfalse; eauto.
    ** destruct (IHes i) as [Htrue|Hfalse].
       *** left. destruct Htrue as ((es', σ')&His).
            (e :: es', σ'). rewrite idx_step_equiv. econstructor.
           rewrite -idx_step_equiv. eauto.
       *** right. intros (c'&Hf). rewrite idx_step_equiv in Hf ×.
           inversion 1. subst. eapply Hfalse. eexists. rewrite idx_step_equiv; eauto.
Qed.

   Lemma idx_step_det (c: cfg ) i c1 c2:
     idx_step i c c1
     idx_step i c c2
     c1 = c2.
   Proof.
     inversion 1 as [e1 c1' e1' cs1 ef1 t1 t2 Heqc Heqc1 Hprim Hlength]; subst.
     inversion 1 as [e2 c2' e2' cs2 ef2 t1' t2' Heqc' Heqc2 Hprim' Hlength']; subst.
     injection Heqc'. clear Heqc'. intros →. intros Heqc'.
     apply app_inj_1 in Heqc' as (->&Heqc'); auto.
     injection Heqc'. clear Heqc'. intros → →.
     repeat f_equal; auto;
     eapply PrimDet; eauto.
   Qed.

Lemma valid_cfg_seq_dec (c: cfg ) ixs:
  { cs | valid_cfg_idx_seq (c :: cs) ixs } + {¬ cs, valid_cfg_idx_seq (c :: cs) ixs}.
Proof.
  revert c.
  induction ixs as [| i ixs].
  - left. []. econstructor.
  - intros c.
    destruct (idx_step_dec' c i) as [(c'&Hs)|Hfalse].
    × destruct (IHixs c') as [(cs'&Hs')|Hfalse'].
      ** left. (c' :: cs'). econstructor; eauto.
      ** right. intros (cs&Hval). inversion Hval as [| |? c'']. subst.
         eapply Hfalse'. assert (c' = c'') by (eapply idx_step_det; eauto).
         subst. eexists; eauto.
    × right. intros (cs&Hval). inversion Hval. subst.
      eapply Hfalse; eauto.
Qed.

  Record interp_codomain := {
    snap_vector: list (refine_cmra K);
    compatible: (big_op snap_vector);
    all_snaps: r, r snap_vector view K (validity_car r) = snapshot;
    all_ne: cfgs K (validity_car (big_op snap_vector)) [];
    all_threads:
       i, i < fold_left max (map (length fst) (cfgs K (validity_car (big_op snap_vector)))) 0
                          i tids K (validity_car (big_op snap_vector))}.


  Definition interp_flat_map (obs: list (refine_cmra K)) n : set nat :=
    {[ i | i (nth n (map (tids K validity_car) obs) ) ]}.

  Lemma last_non_empty: {A: Type} (l: list A), l [] last l None.
  Proof.
    induction l as [| x ?] using rev_ind; rewrite ?last_snoc; congruence.
  Qed.

  Definition interp_flatten (osc: interp_codomain) : cfg × (nat set nat).
  Proof.
    destruct osc as [sv rest ? Hneq_nil ?].
    apply (last_non_empty) in Hneq_nil.
    destruct (last (cfgs K (validity_car (big_op sv)))) as [c|].
    - exact (c, interp_flat_map sv).
    - exfalso; apply (Hneq_nil eq_refl).
  Defined.

  Lemma interp_flatten_last x cs c:
    cfgs K (validity_car (big_op (snap_vector x))) = cs ++ [c]
    fst (interp_flatten x) = c.
  Proof.
    unfold interp_flatten. intros Heq. destruct x as [svx Hcompat ? Hne Hallts ].
    simpl in ×. rewrite Heq in Hcompat Hne Hallts ×.
    clear. generalize (last_non_empty (cs ++ [c]) Hne).
    rewrite last_snoc. auto.
  Qed.

  Lemma interp_flatten_last_inv x:
     cs, cfgs K (validity_car (big_op (snap_vector x))) = cs ++ [fst (interp_flatten x)].
  Proof.
    unfold interp_flatten. destruct x as [svx Hcompat ? Hne Hallts ].
    simpl in ×. clear -Hne.
    destruct (cfgs K (validity_car (big_op svx))) as [| c cs _] using rev_ind;
      first congruence.
     cs.
    generalize (last_non_empty (cs ++ [c]) Hne).
    rewrite last_snoc. auto.
  Qed.

  Lemma interp_flatten_map x:
    snd (interp_flatten x) = interp_flat_map (snap_vector x).
  Proof.
    destruct x as [svx ? ? ?].
    simpl. generalize (last_non_empty _ all_ne0).
    destruct last; last (congruence; done).
    intros. auto.
  Qed.

  Lemma interp_flatten_nth_map_tids x t1 t2 r n:
    snap_vector x = t1 ++ r :: t2
    length t1 = n
    snd (interp_flatten x) n = {[ n | n tids K (validity_car r)]}.
  Proof.
    intros Hsvx Hlen.
    rewrite interp_flatten_map.
    unfold interp_flat_map.
    rewrite Hsvx.
    rewrite map_app.
    rewrite app_nth2.
    - simpl. rewrite map_length Hlen.
      assert (n - n = 0) asby omega; auto.
    - rewrite map_length. subst. econstructor.
  Qed.

  Lemma map_app_inv {A B: Type} (f: A B) (l: list A) (l1 l2: list B):
    map f l = l1 ++ l2 l1' l2', l = l1' ++ l2' map f l1' = l1 map f l2' = l2.
  Proof.
    revert l1 l2. induction l; simpl.
    - intros l1 l2 Heq. symmetry in Heq. apply app_eq_nil in Heq as (->&->).
       [], []; split; auto.
    - intros l1 l2 Heq; destruct l1; simpl in ×.
      × [], (a :: l). split_and!; auto.
      × edestruct (IHl l1 l2) as (l1'&l2'&Heqapp&?&?).
        { inversion Heq; auto. }
        rewrite Heqapp.
         (a :: l1'), l2'; split_and!; auto.
        simpl. inversion Heq; subst. auto.
  Qed.

  Lemma map_cons_inv {A B: Type} (f: A B) (l: list A) (b: B) (l': list B):
    map f l = b :: l' a l0, l = a :: l0 f a = b map f l0 = l'.
  Proof.
    destruct l as [| a l0].
    - simpl; congruence.
    - simpl. intros Heq. a, l0.
      split_and!; inversion Heq; auto.
  Qed.

  Lemma interp_flatten_in_split_sv x n i:
    i (snd (interp_flatten x) n)
     t1 t2 r,
      snap_vector x = t1 ++ r :: t2
      length t1 = n
      (snd (interp_flatten x) n) = {[ n | n tids K (validity_car r) ]}.
  Proof.
    rewrite ?interp_flatten_map.
    intros Hin.
    unfold interp_flat_map in ×.
    case (decide (n < length (map (tids K validity_car) (snap_vector x)))).
    - intros Hlt.
      edestruct (@nth_split _ n (map (tids K validity_car) (snap_vector x))
                            ) as (l1&l2&Heq&Hlen); eauto.
      eapply map_app_inv in Heq as (t1&rt2&Heq&Heq1&Heq2).
      eapply map_cons_inv in Heq2 as (r&t2&Heq'&Heqr&Heq2).
       t1, t2, r. split_and!.
      × rewrite Heq Heq'. auto.
      × rewrite -Heq1 map_length in Hlen. auto.
      × rewrite -Heqr. simpl. auto.
    - intros Hnlt.
      assert (length (map (tids K validity_car) (snap_vector x)) n) by omega.
      erewrite nth_overflow in Hin; auto.
      exfalso. set_solver.
  Qed.

  Lemma interp_flatten_to_natset:
     (x: interp_codomain) j, S: natset, ( n, n S n snd (interp_flatten x) j).
  Proof.
    intros.
    rewrite interp_flatten_map.
    unfold interp_flat_map.
     ( nth j (map (tids K validity_car) (snap_vector x)) ).
    auto.
  Qed.

  Definition interp_step: nat relation (option interp_codomain) := λ i x y,
    match x, y with
    | Some x, Some y
      idx_stepN 1 i (snap_vector x) (snap_vector y)
    | _, _False
    end.

  Definition interp_step': nat relation (interp_codomain) := λ i x y,
      idx_stepN 1 i (snap_vector x) (snap_vector y).

  Require Import ClassicalEpsilon.

  Lemma some_interp_extract:
     (x: interp_codomain) (e: trace interp_step (Some x)),
       (e': trace interp_step' x), fair_pres _ _ e e'.
  Proof.
    intros x e.
    eapply co_se_trace_fair_pres.
    - intros; apply excluded_middle_informative.
    - intros; apply excluded_middle_informative.
    - remember (Some x) as mx. revert mx e x Heqmx.
      cofix.
      intros mx e x.
      destruct e as [i mx y Hstep]. intros →. destruct y as [y|].
      × y. intros i' Henabled. destruct Henabled as (y'&?).
         (Some y'). simpl. auto.
        auto. eauto.
     × inversion Hstep.
  Qed.

  Instance view_eq_dec : (v1 v2: refine_view), Decision (v1 = v2).
  Proof. solve_decision. Defined.

  Instance interp_equiv: Equiv (interp_codomain) := λ x y,
    (snap_vector x snap_vector y).

  Instance interp_equivalence: @Equivalence (interp_codomain) (≡).
  Proof.
    split.
    - intro x. rewrite /equiv /interp_equiv //=.
    - intros x y. rewrite /equiv /interp_equiv //=.
    - intros x y z. rewrite /equiv /interp_equiv //=. intros; etransitivity; eauto.
  Qed.

  Canonical Structure interp_cod_cofeT : cofeT := discreteC (interp_codomain).

  Definition interp (n: nat) (robs: list (iRes Λ (globalF Σ))):
    option interp_codomain.
  Proof.
    pose (sv := map interp_extract robs).
    destruct (excluded_middle_informative ( (big_op sv))); last (exact None).
    destruct (excluded_middle_informative ( r, r sv view K (validity_car r) = snapshot));
      last (exact None).
    case (decide (cfgs K (validity_car (big_op sv)) [])); intros; last (exact None).
    destruct (excluded_middle_informative
      ( i, i < fold_left max (map (length fst) (cfgs K (validity_car (big_op sv)))) 0
                          i tids K (validity_car (big_op sv))));
      last (exact None).
    refine (Some _). econstructor; eauto.
  Defined.

  Existing Instance refine_step.

  Definition force_prop := ( cfg', master_own cfg')%I.

  Instance cfgs_proper Λ K: Proper ((≡) ==> eq) (cfgs Λ K).
  Proof.
    intros r r' Heq.
    inversion Heq. auto.
  Qed.

  Instance idxs_proper Λ K: Proper ((≡) ==> eq) (idxs Λ K).
  Proof.
    intros r r' Heq.
    inversion Heq. auto.
  Qed.

  Instance views_proper Λ K: Proper ((≡) ==> eq) (view Λ K).
  Proof.
    intros r r' Heq.
    inversion Heq. auto.
  Qed.

  Instance tids_proper Λ K: Proper ((≡) ==> eq) (tids Λ K).
  Proof.
    intros r r' Heq.
    inversion Heq. auto.
  Qed.

  Existing Instances validity_equiv validity_valid.
  Lemma validity_car_proper {A: draT} `{Equiv, Valid A} (x y: @validity A) :
     x x y @validity_car A x @validity_car A y.
  Proof.
    inversion 2; auto.
  Qed.

  Instance snap_vector_proper: Proper ((≡) ==> (≡)) snap_vector.
  Proof.
    inversion 1; auto.
    econstructor; eauto.
  Qed.

  Instance map_proper `{Equiv A, !Equivalence (≡), Equiv B, !Equivalence (≡)}:
    Proper (((≡) ==> (≡)) ==> (≡) ==> (≡)) (@map A B).
  Proof.
    intros f f' Heqf l l' Heql.
    induction Heql; simpl; auto.
    constructor; eauto.
  Qed.

  Lemma map_proper' `{Equiv A, !Equivalence (≡), Equiv B, !Equivalence (≡)}:
     (f: A B) l l', l l' ( x y, x l y l' x y f x f y) map f l map f l'.
  Proof.
    intros f l l' Heql Heqf.
    induction Heql; simpl; auto.
    constructor; eauto.
    - eapply Heqf; try left. eauto.
    - eapply IHHeql. intros x' y' Hinl Hink Hequiv. eapply Heqf; try (right; auto).
      eauto.
  Qed.

  Lemma default_id_op {M M': ucmraT} (a b: option M) (Pf: M = M'):
    default (a b) (ucmra_transport Pf)
            default a (ucmra_transport Pf) default b (ucmra_transport Pf).
  Proof.
    destruct a, b; simpl;
    rewrite ?ucmra_transport_op ?right_id ?left_id; auto.
  Qed.

  Lemma interp_extract_op r r':
    interp_extract (r r') interp_extract r interp_extract r'.
  Proof.
    unfold interp_extract.
    rewrite ucmra_transport_op //=.
  Qed.

  Lemma interp_extract_bigop rs:
    interp_extract (big_op rs) big_op (map interp_extract rs).
  Proof.
    induction rs.
    - rewrite /interp_extract //= iprod_lookup_empty.
      symmetry. by rewrite ucmra_transport_unit.
    - rewrite interp_extract_op.
      rewrite IHrs. eauto.
  Qed.

  Existing Instances refine_op refine_equiv refine_equivalence.

  Lemma validity_car_op (a b: refine_cmra K):
    validity_car (a b) = validity_car a validity_car b.
  Proof.
    simpl. auto.
  Qed.

  Lemma cfgs_op_empty (a b: refine_car K):
    cfgs K (a b) = [] cfgs K a = [] cfgs K b = [].
  Proof.
    rewrite /op /refine_op. destruct le_dec as [l|n].
    - simpl. intros Heqnil; split; auto.
      rewrite Heqnil in l.
      destruct (cfgs K a); simpl in *; auto.
      omega.
    - simpl. intros Heqnil. exfalso. rewrite Heqnil in n.
      simpl in ×.
      omega.
  Qed.

  Lemma interp_extract_valid r:
     r interp_extract r.
  Proof.
    unfold interp_extract.
    destruct 1 as (?&?&Hv).
    specialize (Hv (@inG_id Λ Σ _ (refine_inG))).
    by rewrite ucmra_transport_valid.
  Qed.

  Lemma interp_extract_validN r n:
    ✓{n} r ✓{n} interp_extract r.
  Proof.
    unfold interp_extract.
    destruct 1 as (?&?&Hv).
    specialize (Hv (@inG_id Λ Σ _ (refine_inG))).
    by rewrite ucmra_transport_validN; eauto.
  Qed.

  Lemma interp_extract_stepN r1 r2 n:
    r1 _(n) r2 interp_extract r1 _(n) interp_extract r2.
  Proof.
    unfold interp_extract.
    intros Hv.
    specialize (Hv (@inG_id Λ Σ _ (refine_inG))).
    by rewrite ucmra_transport_stepN; eauto.
  Qed.

  Lemma interp_extract_big_op_validN rs n:
    ✓{n} (big_op rs) ✓{n} big_op (map interp_extract rs).
  Proof.
    rewrite -interp_extract_bigop.
    apply interp_extract_validN.
  Qed.

  Lemma interp_extract_big_op_valid rs:
     (big_op rs) big_op (map interp_extract rs).
  Proof.
    rewrite -interp_extract_bigop.
    apply interp_extract_valid.
  Qed.

  Lemma interp_extract_big_op_validN' rs n:
    ✓{n} (big_op rs) big_op (map interp_extract rs).
  Proof.
    rewrite -interp_extract_bigop.
    apply interp_extract_validN.
  Qed.


   Lemma isteps_det (c: cfg ) idxs c1 c2:
     isteps (idx_step) idxs c c1
     isteps (idx_step) idxs c c2
     c1 = c2.
   Proof.
     revert c.
     induction idxs; intros c.
     - inversion 1. subst.
       inversion 1. subst. auto.
     - inversion 1 as [|? ? ? c1' ?]. subst.
       inversion 1 as [|? ? ? c2' ?]. subst.
       assert (c1' = c2') by (eapply idx_step_det; eauto). subst.
       eapply IHidxs; eauto.
   Qed.

Lemma valid_seq_inj2 c cs1 cs2 is1:
  valid_cfg_idx_seq ([c] ++ cs1) is1
  valid_cfg_idx_seq ([c] ++ cs2) is1
  cs1 = cs2.
Proof.
  revert c cs1 cs2.
   induction is1. simpl.
   - intros c cs1 cs2.
     inversion 1; subst.
     inversion 1; subst. auto.
   - intros c cs1 cs2.
     inversion 1 as [| |? c1']; subst.
     inversion 1 as [| |? c2']; subst. auto.
     assert (c1' = c2') asby (eapply idx_step_det; eauto).
     f_equal. eauto.
Qed.

Lemma valid_seq_inj2' cinit c cs1 cs2 is1:
  valid_cfg_idx_seq (cinit ++ [c] ++ cs1) is1
  valid_cfg_idx_seq (cinit ++ [c] ++ cs2) is1
  cs1 = cs2.
Proof.
  intros Hval1 Hval2.
  assert (length (cinit ++ [c] ++ cs1) = S (length is1)) as Hlen1.
  { edestruct valid_cfg_idx_length3 as [(?&Hlen_bad)|]; first eapply Hval1; auto.
    rewrite app_length in Hlen_bad. simpl in ×. omega.
  }
  assert (length (cinit ++ [c] ++ cs2) = S (length is1)) as Hlen2.
  { edestruct valid_cfg_idx_length3 as [(?&Hlen_bad)|]; first eapply Hval2; auto.
    rewrite app_length in Hlen_bad. simpl in ×. omega.
  }
  eapply valid_seq_app in Hval1 as (is1a&is1b&Heq1&?).
  eapply valid_seq_app in Hval2 as (is1a'&is1b'&Heq1'&?).
  assert (length cs1 = length cs2) as Hlencs. rewrite ?app_length in Hlen1 Hlen2; omega.
  subst.
  assert (length is1b' = length is1b).
  erewrite <-(valid_cfg_idx_length5); eauto.
  rewrite -Hlencs.
  eapply valid_cfg_idx_length5; eauto.
  apply app_inj_2 in Heq1' as (?&?); auto.
  subst. eapply valid_seq_inj2; eauto.
Qed.

    Lemma app_eq_disjoint_set:
       is1 is2 is1' is2' (tset: natset),
        is1 ++ is2 = is1' ++ is2'
        ( i, i is1 i tset)
        ( i, i is1' i tset)
        ( i, i is2 i tset)
        ( i, i is2' i tset)
        is1 = is1'.
    Proof.
      induction is1 as [| i is1].
      - induction is1' as [| i' is1']; auto.
        intros is2' tset Heq.
        destruct is2 as [| i is2]; first (simpl in *; congruence).
        simpl in ×. assert (i = i') asby (inversion Heq; auto).
        intros ? Hnint Hint ?.
        exfalso.
        apply (Hnint i'); first (left).
        apply Hint. left.
      - induction is1' as [| i' is1']; auto.
        × intros is2' tset Heq.
          destruct is2' as [| i' is2']; first (simpl in *; congruence).
          simpl in ×. assert (i = i') asby (inversion Heq; auto).
          intros Hnint ? ? Hint.
          exfalso.
          apply (Hnint i'); first (left).
          apply Hint. left.
        × intros is2' tset Heq Hnin Hnin' Hin Hin'.
          simpl in Heq. inversion Heq.
          f_equal.
          edestruct (IHis1 is2 is1' is2'); eauto.
          ** intros. eapply Hnin. right. auto.
          ** intros. eapply Hnin'. right. auto.
    Qed.

  Lemma refine_step_det_idx r r' r'':
    refine_step K r r' refine_step K r r''
    idxs K r' = idxs K r'' r' = r''.
  Proof.
    intros (cs0&c1&c2&cspec&csext&i'&ispec&ixs&Heqcsr&Hviewr'&Heqcsr'&Heqidxsr'
            &?&?&?&Htids'&Hval')%refine_step_inv.
    intros (cs0'&c1'&c2'&cspec'&csext'&i''&ispec'&ixs'&Heqcsr_alt&Hviewr''&Heqcsr''&
            Heqidxsr''&?&?&?&Htids''&Hval'')%refine_step_inv.
    intros Heq_idxs.
    rewrite Heqcsr in Heqcsr_alt. apply app_inj_2 in Heqcsr_alt as (?&Heqc1); auto.
    inversion Heqc1; subst.
    rewrite -Heq_idxs Heqidxsr' in Heqidxsr''.
    apply app_inv_head in Heqidxsr''. subst.
    rewrite Heqidxsr'' in Hval'.
    assert (cspec ++ csext ++ [c2] = cspec' ++ csext' ++ [c2']) as Heqcs2.
    { eapply valid_seq_inj2; eauto 20. }
    assert (c2 = c2') as →.
    { rewrite ?app_assoc in Heqcs2. apply app_inj_2 in Heqcs2 as (?&Heqc); auto.
      inversion Heqc; auto. }
    assert (ispec = ispec') as →.
    { eapply app_eq_disjoint_set; eauto. }
    apply app_inj_1 in Heqcs2 as (Heqcspec&Heqcsext); last (congruence); [].
    apply app_inv_tail in Heqcsext.
    subst.
    destruct r', r''; simpl in ×.
    f_equal; try congruence.
    - apply mapset_eq.
      intros i; split; intros Hin.
      × rewrite Htids'' -Htids'; auto.
      × rewrite Htids' -Htids''; auto.
  Qed.

  Lemma interp_extract_validN' r n:
    ✓{S n} r interp_extract r.
  Proof.
    intros (?&?&Hv). cut (✓{S n} (interp_extract r)); auto.
    unfold interp_extract.
    specialize (Hv (@inG_id Λ Σ _ (refine_inG))).
    by rewrite ucmra_transport_validN; eauto.
  Qed.

  Lemma op_longer (a x: refine_cmra K):
     (a x)
    idxs K (validity_car a) `prefix_of` idxs K (validity_car x)
    idxs K (validity_car a validity_car x) = idxs K (validity_car x).
  Proof.
    intros Hval_op Hprefix.
    assert ( a).
    { by eapply cmra_valid_op_l. }
    assert ( x).
    { by eapply cmra_valid_op_r. }
    destruct a as [a ? vpa].
    destruct x as [x ? vpx].
    apply refine_disjoint_prefix_idxs.
    - eapply vpa; eauto.
    - eapply vpx; eauto.
    - destruct Hval_op as (?&?&?); auto.
    - simpl. auto.
  Qed.

  Lemma step_longer (x y x': refine_cmra K) n:
     (x y)
    x _(n) x'
     (x' y)
    view K (validity_car y) = snapshot
    idxs K (validity_car y) `prefix_of` idxs K (validity_car x').
  Proof.
    destruct x as [x ? vpx].
    destruct y as [y ? vpy].
    destruct x' as [x' ? vpx'].
    intros (Hvalx&Hvaly&Hdisjxy).
    intros (_&Hstep).
    specialize (Hstep Hvalx).
    intros (Hvalx'&_&Hdisjx'y).
    intros Hview.
    eapply vpx in Hvalx.
    eapply vpy in Hvaly.
    eapply vpx' in Hvalx'.
    simpl in ×.
    clear vpx vpy vpx'.
    inversion Hdisjxy as [t1 t2 cs1 cs2 is1 is2 Hinter [Hprefix|Hprefix]| |]; subst; simpl in ×.
    - eapply refine_step_inv in Hstep as
          (cs0&c1&c2&cspec&csext&i'&ispec&ixs&Heqcsr&Hviewr'&
           Heqcsr'&Heqidxsr' &?&?&Hin&Htids'&Hval'); simpl in ×.
      destruct x'; simpl in *; subst.
      inversion Hdisjx'y as [t1' t2' cs1' cs2' is1' is2' Hinter' [Hprefix'|Hprefix']| |];
        subst; simpl in ×.
      × exfalso.
        destruct Hprefix as (_&ispec0&Heqspec0&Hnin0).
        rewrite Heqspec0 in Hprefix'.
        destruct Hprefix' as (_&ispec1&Heqspec1&Hnin1).
        rewrite -app_assoc in Heqspec1.
        apply app_inv_head in Heqspec1.
        apply (Hnin0 i'); first (apply Hin; set_solver+).
        subst. set_solver+.
      × destruct Hprefix' as (?&?&?&?).
        eexists. eauto.
    - destruct Hprefix as (?&iext1&?&?).
      eapply refine_step_inv in Hstep as
          (cs0&c1&c2&cspec&csext&i'&ispec&ixs&Heqcsr&Hviewr'
           &Heqcsr'&Heqidxsr' &?&?&Hin&Htids'&Hval'); simpl in ×.
      destruct x'; simpl in *; subst.
      rewrite -?app_assoc.
      eexists; eauto.
    - simpl in ×. congruence.
    - simpl in ×. inversion Hstep.
  Qed.

  Lemma validity_car_op_comm (a b: refine_cmra K):
    validity_car (a b) = validity_car a validity_car b.
  Proof. auto. Qed.

  Lemma big_op_longest_aux (l: list (refine_cmra K)) (x: refine_cmra K):
     (big_op (x :: l))
    ( (r: refine_cmra K),
        r x :: l idxs K (validity_car r) `prefix_of` idxs K (validity_car x))
    idxs K (validity_car (big_op (x :: l))) = idxs K (validity_car x).
  Proof.
    induction l as [| a l].
    - intros. simpl big_op. rewrite validity_car_proper; eauto. by rewrite right_id.
    - intros Hval Hin_small. simpl big_op.
      rewrite (validity_car_proper (x (a big_op l))
                                   (a (x big_op l))); eauto.
      × rewrite validity_car_op_comm.
         rewrite op_longer; eauto.
         ** simpl in Hval. eapply IHl; eauto.
            intros r Hin. eapply Hin_small.
            inversion Hin; subst; auto.
            *** left.
            *** do 2 right; auto.
         ** simpl in ×.
            erewrite IHl; eauto.
            *** apply Hin_small. right; left.
            *** intros r Hin. eapply Hin_small.
                inversion Hin; subst; auto.
              **** left.
              **** do 2 right; auto.
      × rewrite ?assoc. rewrite (comm _ x). auto.
  Qed.

  Lemma permutation_hd {A: Type} (l: list A) x:
    x l l', Permutation (x :: l') l.
  Proof.
    induction l.
    - inversion 1.
    - inversion 1 as [| Hin_rec]; subst.
      × l; eauto.
      × edestruct IHl as (l'&HPerm); auto.
         (a :: l').
        eapply perm_trans; first eapply perm_swap.
        econstructor; eauto.
  Qed.

  Lemma big_op_longest l (x: refine_cmra K):
     (big_op l)
    x l
    ( r : refine_cmra K, r l idxs K (validity_car r) `prefix_of` idxs K (validity_car x))
    idxs K (validity_car (big_op l)) = idxs K (validity_car x).
  Proof.
    intros Hval Hin Hin_small; edestruct (permutation_hd l x) as (l'&Heql'); eauto.
    rewrite (validity_car_proper (big_op l) (big_op (x :: l'))); last (rewrite Heql'); eauto.
    eapply big_op_longest_aux; eauto.
    × rewrite Heql'. auto.
    × intros. eapply Hin_small. rewrite -Heql'. auto.
  Qed.

  Lemma elem_of_equiv_list `{Equiv A} a (l l': list A):
    l l' a l a', a' l' a a'.
  Proof.
    revert a. induction 1.
    - set_solver+.
    - intros [Heqx|Hinl]%elem_of_cons.
      × subst. eexists; split; first left; eauto.
      × edestruct IHlist_equiv as (a'&?&?); eauto.
         a'. split; first right; eauto.
  Qed.

  Lemma elem_of_big_op_compat (l1 l2: list (refine_cmra K)) (r: refine_cmra K):
     (big_op (l1 ++ r :: l2))
     r', r' l1 (r' r).
  Proof.
    induction l1; simpl; intros Hval r' Hin; first set_solver.
    apply elem_of_cons in Hin as [Heq|Hinl1]. subst.
    - rewrite big_op_app in Hval ×. simpl. auto.
    - eapply IHl1; eauto.
  Qed.

  Lemma elem_of_big_op_compat' (l1 l2: list (refine_cmra K)) (r: refine_cmra K):
     (big_op (l1 ++ r :: l2))
     r', r' l2 (r' r).
  Proof.
    induction l2; simpl; intros Hval r' Hin; first set_solver.
    apply elem_of_cons in Hin as [Heq|Hinl2]. subst.
    - rewrite big_op_app in Hval ×. simpl. auto.
    - eapply IHl2; auto. rewrite ?big_op_app in Hval ×. simpl. eauto.
  Qed.

  Lemma subseteq_union_decompose:
     (A B C: natset), A B C B' C', B' B C' C A B' C'.
  Proof.
    intros A B C Hsub_union.
     (A B), (A C).
    split_and!.
    - eapply intersection_subseteq_r.
    - eapply intersection_subseteq_r.
    - rewrite -(@intersection_union_l _ _ _ _ _).
      symmetry. apply subseteq_intersection_1; auto.
  Qed.

  Lemma subseteq_singleton (A: natset) n:
    A {[n]} A A {[n]}.
  Proof.
    case (decide (n A)).
    - intros Hin Hsub. right. split; auto. apply elem_of_subseteq_singleton; auto.
    - intros Hnin Hsub. left. split; auto.
      × intros HinA.
        exfalso.
        assert (x = n). eapply (proj1 (elem_of_subseteq A {[n]}) Hsub) in HinA.
        apply elem_of_singleton_1 in HinA. auto.
        subst. eapply Hnin. eauto.
      × set_solver.
  Qed.

  Lemma natset_powerset_finite:
     (A: natset), set_finite {[ B | B A ]}.
  Proof.
    intros A.
    eapply (collection_ind (λ A, set_finite {[ B | B A]})).
    × intros A' A'' Hequiv.
      rewrite leibniz_equiv_iff in Hequiv ×. intros →. auto.
    × []. intros B Hin.
      cut (B = ); intros; subst; first left.
      apply mapset_eq.
      intros b. split.
      ** assert (B ) by set_solver. auto.
      ** set_solver.
    × intros x X Hnin IHfin.
      destruct IHfin as (l&Hinl).
       (map (union {[x]}) l ++ l).
      intros C. intros Hsub'.
      assert (C {[x]} X) by set_solver.
      edestruct subseteq_union_decompose as (B'&C'&Hsub1&Hsub2&Hequiv); eauto.
      edestruct subseteq_singleton as [Hempty|Hsingle]; eauto.
      ** rewrite Hempty in Hequiv ×. rewrite left_id; intros Hequiv.
         apply elem_of_app. right. eapply Hinl.
         by rewrite -Hequiv in Hsub2 ×.
      ** apply elem_of_app. left.
         rewrite Hsingle in Hequiv ×. rewrite leibniz_equiv_iff.
         intros; subst.
         eapply elem_of_map. eapply Hinl. eauto.
  Qed.

  Fixpoint ns_leq_aux (n: nat) :=
    match n with
    | Otrue :: nil
    | S n'true :: ns_leq_aux n'
    end.

  Definition ns_leq (n: nat): natset :=
    of_bools (ns_leq_aux n).

  Lemma ns_leq_spec n:
     n', n' n n' ns_leq n.
  Proof.
    intros n'. rewrite elem_of_of_bools.
    revert n'. induction n.
    - intros. induction n'; simpl; split; auto.
      ** omega.
      ** inversion 1.
    - intros. induction n'; simpl; split; auto.
      ** omega.
      ** intros; eapply IHn. omega.
      ** rewrite -IHn. omega.
  Qed.

  Lemma set_finite_flatten A (X: set A) (Y: list (set A)):
    ( X', X' Y set_finite X')
    ( x, x X X', X' Y x X')
    set_finite X.
  Proof.
    intros Hall_fin Hin.
    assert ( Xrest, set_finite Xrest
                      ( x : A, x X x Xrest
                                          X' : set A, X' Y x X' Xrest)) as Hin'.
    {
       .
      split.
      - apply empty_finite.
      - intros x HinX. edestruct (Hin x) as (X'&?&?); eauto.
        right. X'. rewrite right_id. auto.
    }
    clear Hin. revert X Hall_fin Hin'.
    induction Y as [| X' Y IHY].
    - intros X ? Hin.
      edestruct Hin as (Xrest&?&Hin').
      apply (set_finite_subseteq Xrest); auto.
      intros x HinX.
      edestruct (Hin' x) as [Hin_rest|(X'&Hfalse&?)]; eauto.
      set_solver.
    - intros X Hall_fin Hin.
      eapply IHY.
      × intros X'' HinY. eapply Hall_fin. right; auto.
      × destruct Hin as (Xrest&Hfin_rest&Hcover).
         (X' Xrest); split.
        ** apply union_finite; auto. apply Hall_fin. left.
        ** intros x HinX. edestruct Hcover as [Hin_rest|(X''&HinY&HinU)]; eauto.
           *** left. clear -Hin_rest. set_solver.
           *** inversion HinY; subst; auto.
               right. X''. split; auto. clear -HinU. set_solver.
  Qed.

  Lemma union_finite_setoid `{Equiv A, Equivalence A} (X Y: set A):
    set_finite_setoid X
    set_finite_setoid Y
    set_finite_setoid (X Y).
  Proof.
    intros (l&Hinl) (k&Hink).
     (l ++ k). intros x [HinX|HinY].
    - edestruct Hinl as (x'&?&?); eauto.
       x'; split; eauto. apply elem_of_app; left; auto.
    - edestruct Hink as (x'&?&?); eauto.
       x'; split; eauto. apply elem_of_app; right; auto.
  Qed.

  Lemma set_finite_setoid_flatten `{Equiv A, Equivalence A (≡)} (X: set A) (Y: list (set A)):
    ( X', X' Y set_finite_setoid X')
    ( x, x X X', X' Y x X')
    set_finite_setoid X.
  Proof.
    intros Hall_fin Hin.
    assert ( Xrest, set_finite_setoid Xrest
                      ( x : A, x X x Xrest X' : set A, X' Y x X' Xrest)) as Hin'.
    {
       .
      split.
      - []; intros x; set_solver+.
      - intros x HinX. edestruct (Hin x) as (X'&?&?); eauto.
        right. X'. rewrite right_id. auto.
    }
    clear Hin. revert X Hall_fin Hin'.
    induction Y as [| X' Y IHY].
    - intros X ? Hin.
      edestruct Hin as (Xrest&?&Hin').
      apply (set_finite_setoid_subseteq Xrest); auto.
      intros x HinX.
      edestruct (Hin' x) as [Hin_rest|(X'&Hfalse&?)]; eauto.
      set_solver.
    - intros X Hall_fin Hin.
      eapply IHY.
      × intros X'' HinY. eapply Hall_fin. right; auto.
      × destruct Hin as (Xrest&Hfin_rest&Hcover).
         (X' Xrest); split.
        ** apply union_finite_setoid; auto. apply Hall_fin. left.
        ** intros x HinX. edestruct Hcover as [Hin_rest|(X''&HinY&HinU)]; eauto.
           *** left. clear -Hin_rest. set_solver.
           *** inversion HinY; subst; auto.
               right. X''. split; auto. clear -HinU. set_solver.
  Qed.

  Lemma exists_list_choice {A B} (l: list A) (P: A B Prop):
    ( a, a l b, P a b)
     (l': list (A×B)), a, a l b, (a, b) l' P a b.
  Proof.
    revert P.
    induction l. intros.
    - []. intros a. inversion 1.
    - intros P Hin.
      edestruct IHl as (l'&Hinl').
      { intros a' Hin'. eapply Hin. right. eauto. }
      edestruct (Hin a) as (b&?); first (left).
       ((a, b) :: l').
      intros a'. inversion 1; subst; auto.
      × eexists. split; first left; eauto.
      × edestruct Hinl' as (?&?&?); eauto.
        eexists. split; first right; eauto.
  Qed.

  Lemma exists_list_choice' {A B} (l: list A) (P: A B Prop) (Q: B Prop):
    ( a, a l b, P a b)
    ( a b, P a b Q b)
    ( b, Q b)
     (l': list (A×B)), ( a, a l b, (a, b) l' P a b)
      b, ( a, (a, b) l') Q b.
  Proof.
    induction l. intros.
    - []. split.
      × intros a. inversion 1.
      × intros b (a&Hin). inversion Hin.
    - intros Hin HPQ Hsomeb.
      edestruct IHl as (l'&Hinl'&Hinl'2); eauto.
      { intros a' Hin'. eapply Hin. right. eauto. }
      edestruct (Hin a) as (b&?); first (left).
       ((a, b) :: l'); split.
      × intros a'. inversion 1; subst; auto.
        ** eexists. split; first left; eauto.
        ** edestruct Hinl' as (?&?&?); eauto.
           eexists. split; first right; eauto.
      × intros b' (a'&Hin').
        inversion Hin'; subst; eauto.
  Qed.

  Lemma set_finite_quotient A A' (f: A A')
        (X: set A) (Y: set A') (f_in: x, x X f x Y)
        (f_blocks: y, X', set_finite X' x, x X f x = y x X'):
        set_finite Y
        set_finite X.
  Proof.
    intros (l&Hfin_in).
    edestruct (exists_list_choice' l (λ y X', set_finite X' ( x, x X f x = y x X'))
                                   set_finite)
              as (l'&Hin_l'&Hin_l'2).
    { intros y Hin. edestruct (f_blocks y); eauto. }
    { simpl. intros ? ? (?&?); auto. }
    { ; apply empty_finite. }
    eapply (set_finite_flatten _ _ (map snd l')).
    - intros X'.
      intros (ab&?&?)%elem_of_map_inv.
      eapply Hin_l'2. destruct ab. simpl in ×. subst. eexists; eauto.
    - intros x HinX.
      specialize (f_in x HinX).
      specialize (Hfin_in _ f_in).
      edestruct (Hin_l' (f x)) as (X'&Hsnd&Hfin&Hin_block); eauto.
       X'. split.
      × replace X' with (snd (f x, X')); last auto. eapply elem_of_map.
        eauto.
      × eapply Hin_block; eauto.
  Qed.

  Lemma set_finite_setoid_quotient `{Equiv A, Equivalence A (≡), Equiv A', Equivalence A (≡)}
        (f: A A') (X: set A) (Y: set A') (f_in: x, x X f x Y)
        (f_blocks: y, X', set_finite_setoid X' x, x X f x y x X'):
        set_finite_setoid Y
        set_finite_setoid X.
  Proof.
    intros (l&Hfin_in).
    edestruct (exists_list_choice' l (λ y X', set_finite_setoid X' ( x, x X f x y x X'))
                                   set_finite_setoid)
              as (l'&Hin_l'&Hin_l'2).
    { intros y Hin. edestruct (f_blocks y); eauto. }
    { simpl. intros ? ? (?&?); auto. }
    { . []. intros x. set_solver+. }
    eapply (set_finite_setoid_flatten _ (map snd l')).
    - intros X'.
      intros (ab&?&?)%elem_of_map_inv.
      eapply Hin_l'2. destruct ab. simpl in ×. subst. eexists; eauto.
    - intros x HinX.
      specialize (f_in x HinX).
      specialize (Hfin_in _ f_in).
      edestruct Hfin_in as (x'&?&?).
      edestruct (Hin_l' x') as (X'&Hsnd&Hfin&Hin_block); eauto.
       X'. split.
      × replace X' with (snd (x', X')); last auto. eapply elem_of_map.
        eauto.
      × eapply Hin_block; eauto.
  Qed.

  Lemma set_finite_setoid_quotient_strong `{Equiv A, Equivalence A (≡), Equiv A', Equivalence A (≡)}
        (f: A option A') (X: set A) (Y: set A') (f_in: x, x X y, f x = Some y y Y)
        (f_blocks: y, X', set_finite_setoid X' x, x X f x Some y x X'):
        set_finite_setoid Y
        set_finite_setoid X.
  Proof.
    intros (l&Hfin_in).
    edestruct (exists_list_choice' l (λ y X', set_finite_setoid X'
                                               ( x, x X f x Some y x X'))
                                   set_finite_setoid)
              as (l'&Hin_l'&Hin_l'2).
    { intros y Hin. edestruct (f_blocks y); eauto. }
    { simpl. intros ? ? (?&?); auto. }
    { . []. intros x. set_solver+. }
    eapply (set_finite_setoid_flatten _ (map snd l')).
    - intros X'.
      intros (ab&?&?)%elem_of_map_inv.
      eapply Hin_l'2. destruct ab. simpl in ×. subst. eexists; eauto.
    - intros x HinX.
      specialize (f_in x HinX).
      destruct f_in as (y & Heq & HyIn).
      specialize (Hfin_in _ HyIn).
      edestruct Hfin_in as (x'&?&?).
      edestruct (Hin_l' x') as (X'&Hsnd&Hfin&Hin_block); eauto.
       X'. split.
      × replace X' with (snd (x', X')); last auto. eapply elem_of_map.
        eauto.
      × eapply Hin_block; eauto.
        rewrite Heq. econstructor; eauto.
  Qed.

  Lemma set_finite_product {X Y} (A: set X) (B: set Y):
    set_finite A
    set_finite B
    set_finite {[ AB | fst AB A snd AB B]}.
  Proof.
    intros HfinA HfinB.
    apply (set_finite_quotient _ _ snd _ B).
    - intros x. inversion 1. auto.
    - intros y. ({[ ab | fst ab A snd ab = y]}).
      split.
      × destruct HfinA as (l&Hinl).
         (map (λ a, (a, y)) l).
        intros x. inversion 1. subst.
        destruct x; subst. simpl.
        eapply (elem_of_map (λ a:X, (a, y)) _ x).
        eauto.
      × intros x. inversion 1. subst. intros.
        subst. split; auto.
    - auto.
  Qed.

  Existing Instance prod_equiv.
  Instance pair_equivalence `{Equiv A, @Equivalence A (≡), Equiv B, @Equivalence B (≡)} :
    @Equivalence (A × B)%type (≡).
  Proof. eapply prod_relation_equiv; apply _. Qed.

  Lemma set_finite_setoid_product `{Equiv X, @Equivalence X (≡), Equiv Y, @Equivalence Y (≡)}
        (A: set X) (B: set Y):
    set_finite_setoid A
    set_finite_setoid B
    @set_finite_setoid (X×Y) prod_equiv _ _ {[ AB | fst (AB: X × Y) A snd AB B]}.
  Proof.
    intros HfinA HfinB.
    apply (set_finite_setoid_quotient snd _ B).
    - intros x. inversion 1. auto.
    - intros y. ({[ ab | fst ab A snd ab y]}).
      split.
      × destruct HfinA as (l&Hinl).
         (map (λ a, (a, y)) l).
        intros x. inversion 1. subst.
        destruct x; subst. simpl.
        edestruct (Hinl x) as (x'&Hequiv&Hin); eauto.
         (x', y). split; auto.
        ** econstructor; auto.
        ** eapply (elem_of_map (λ a:X, (a, y)) _ x'). eauto.
      × intros x. inversion 1. subst. intros.
        subst. split; auto.
    - auto.
  Qed.

  Lemma natmap_split_finite:
     (A: natset), set_finite {[ BC | fst BC snd BC = A]}.
  Proof.
    intros A.
    eapply (set_finite_subseteq {[ AB | fst AB {[ B | B A ]} snd AB {[ B | B A ]}]}).
    - intros BC. inversion 1; subst.
      split; set_solver+.
    - apply set_finite_product; apply natset_powerset_finite.
  Qed.

  Lemma elem_of_big_op_valid:
     l (x: refine_cmra K), (big_op l) x l x.
  Proof.
    induction 2; auto.
  Qed.

  Lemma set_finite_square {X} (A: set X):
    set_finite A
    set_finite {[ AA | fst AA A snd AA A]}.
  Proof.
    intros; apply set_finite_product; auto.
  Qed.

  Lemma set_finite_product3 {X Y Z} (A: set X) (B: set Y) (C: set Z):
    set_finite A
    set_finite B
    set_finite C
    set_finite {[ ABC | fst (fst ABC) A snd (fst ABC) B
                         snd (ABC) C]}.
  Proof.
    intros.
    apply (set_finite_subseteq {[ ABC | (fst ABC) {[ AB | fst AB A snd AB B]}
                                        (snd ABC) C]}).
    - intros ABC (Hin1&Hin2&Hin3).
      split; auto.
      split; auto.
    - apply set_finite_product; auto.
      apply set_finite_product; auto.
  Qed.

  Lemma set_finite_setoid_product3
        `{Equiv X, @Equivalence X (≡), Equiv Y, @Equivalence Y (≡), Equiv Z, @Equivalence Z (≡)}
        (A: set X) (B: set Y) (C: set Z):
    set_finite_setoid A
    set_finite_setoid B
    set_finite_setoid C
    @set_finite_setoid (X × Y × Z) _ _ _ {[ ABC | fst (fst ABC) A snd (fst ABC) B
                         snd (ABC) C]}.
  Proof.
    intros.
    apply (set_finite_setoid_subseteq {[ ABC | (fst ABC) {[ AB | fst AB A snd AB B]}
                                        (snd ABC) C]}).
    - intros ABC (Hin1&Hin2&Hin3).
      split; auto.
      split; auto.
    - apply set_finite_setoid_product; auto.
      apply set_finite_setoid_product; auto.
  Qed.

  Lemma prefix_set_finite A (l: list A):
    set_finite {[ l' | l' `prefix_of` l]}.
  Proof.
    induction l as [| a l].
    - [[]]. intros l.
      inversion 1 as (lext&Heq).
      symmetry in Heq.
      apply app_eq_nil in Heq as (?&?).
      subst. econstructor.
    - destruct IHl as (L&Hin_L).
       ([] :: (map (cons a) L)).
      intros l'.
      inversion 1 as (lext&Heq).
      destruct l' as [|a' l''].
      ** left.
      ** rewrite -app_comm_cons in Heq.
         inversion Heq; subst.
         right. eapply elem_of_map.
         apply Hin_L. lext. eauto.
  Qed.

  Existing Instances refine_disjoint refine_valid refine_equiv refine_equivalence.
  Lemma set_finite_refine_car_split (x: refine_car K):
    set_finite {[ ab | (fst ab) (snd ab) fst ab snd ab fst ab snd ab = x]}.
  Proof.
    apply (set_finite_subseteq {[ ab | fst ab {[ y | cfgs K y `prefix_of` cfgs K x
                                                       idxs K y `prefix_of` idxs K x
                                                       tids K y tids K x]}
                                       snd ab {[ y | cfgs K y `prefix_of` cfgs K x
                                                       idxs K y `prefix_of` idxs K x
                                                       tids K y tids K x]}]}).
    - simpl.
      intros ab. destruct 1 as ((Hvala&?)&(Hvalb&?)&Hdisj&Hop).
      destruct ab as (a, b). simpl in ×.
      assert (b a = x) as Hop'.
      {
        rewrite -Hop.
        destruct (refine_dra K).
        symmetry.
        by rewrite dra_comm.
      }

      specialize (prefix_of_valid_seq_op K a b).
      intros pop.
      inversion Hdisj as [ | | ]; subst; simpl in ×.
      × edestruct pop as [(Hprefix&->)|(Hprefix&->)]; eauto; simpl; clear pop.
        ** split; econstructor; simpl; eauto.
           *** destruct Hprefix as (?&?&?&?); eauto.
           *** destruct Hprefix as (?&?&?&?). split.
               **** eexists; eauto.
               **** set_solver+.
           *** split; eauto. set_solver+.
        ** split; econstructor; simpl; eauto.
           *** split; eauto. set_solver+.
           *** destruct Hprefix as (?&?&?&?); eauto.
           *** destruct Hprefix as (?&?&?&?). split.
               **** eexists; eauto.
               **** set_solver+.
      × clear pop.
        rewrite prefix_of_op; last (eexists; eauto; done).
        simpl. split; econstructor; try split; simpl;
        try (auto; eexists; eauto);
        try (set_solver+).
      × clear pop. rewrite -Hop'.
        rewrite prefix_of_op; last (eexists; eauto; done).
        simpl. split; econstructor; try split; simpl;
        try (auto; eexists; eauto);
        try (set_solver+).
    - apply set_finite_square.
      eapply (set_finite_quotient _ _ (λ r, (cfgs K r, idxs K r, tids K r)) _
                                  ({[ it | fst (fst it) {[ i | i `prefix_of` cfgs K x]}
                                           snd (fst it) {[ i | i `prefix_of` idxs K x]}
                                           snd it {[ ts | ts tids K x]}]})).
      × intros r; destruct 1 as (?&?&?). split; simpl; auto.
      × intros ((cs, ixs), ts).
         ({[ Refine K master ts cs ixs]}
                   {[ Refine K snapshot ts cs ixs]}).
        split.
        ** apply union_finite; apply singleton_finite.
        ** intros r. destruct 1 as (Hpre1&Hpre2&Hsub).
           destruct r. simpl.
           inversion 1; subst.
           destruct view; auto; set_solver+.
      × apply set_finite_product3.
        ** eapply prefix_set_finite.
        ** eapply prefix_set_finite.
        ** eapply natset_powerset_finite.
  Qed.

  Lemma set_finite_implies_setoid `{Equiv A, Equivalence A (≡)} (X: set A):
    set_finite X set_finite_setoid X.
  Proof.
    intros (l&Hin).
     l. intros x HinX. x. split; eauto.
  Qed.

  Lemma set_finite_list_cons {A: Type} (X: set A) (Y: set (list A)):
    set_finite X
    set_finite Y
    set_finite {[ xs | x xs', xs = x :: xs'
                                x X
                                xs' Y]}.
  Proof.
    intros HfinX HfinY.
    edestruct HfinX as [l Hinl].
    destruct l as [| x l].
    - [].
      intros xs. set_unfold. intros (x&?&?&?&?). eapply Hinl; eauto.
    - eapply (set_finite_quotient _ _ (λ xs, match xs with
                                             | [](x, [])
                                             | x' :: tl(x', tl)
                                             end)
                                  _
                                  {[ ab | fst ab X snd ab Y]});
      last eapply set_finite_product; eauto.
      × intros xs (?&?&?&?&?).
        subst. set_unfold; auto.
      × intros (x', xs').
         {[x' :: xs']}. split; first apply singleton_finite.
        intros xs'' (?&?&?&?&?). subst. inversion 1. set_unfold. auto.
  Qed.

  Definition setoid_closure `{Equiv A} (X: set A) : set A := {[ x | x', x' X x x']}.
  Lemma setoid_closure_pres_fin `{Equiv A, Equivalence A (≡)} (X: set A):
    set_finite_setoid (setoid_closure X) set_finite_setoid X.
  Proof.
    split.
    - intros (l&Hinl).
       l. intros x HinX.
      edestruct (Hinl x) as (x'&?&?).
      { unfold setoid_closure; set_unfold. eexists; split; eauto. }
       x'; split; auto.
    - intros (l&Hinl).
       l. intros x HinX.
      inversion HinX as (x'&?&?).
      edestruct (Hinl x') as (x''&?&?).
      { unfold setoid_closure; set_unfold; eauto. }
       x''. split; eauto. etransitivity; eauto.
  Qed.

  Existing Instances list_equiv list_equivalence.
  Lemma set_finite_setoid_list_cons `{Equiv A, Equivalence A (≡)} (X: set A) (Y: set (list A)):
    set_finite_setoid X
    set_finite_setoid Y
    set_finite_setoid {[ xs | x xs', (xs: list A) x :: xs'
                                x X
                                xs' Y]}.
  Proof.
    intros HfinX HfinY.
    edestruct HfinX as [l Hinl].
    destruct l as [| x l].
    - [].
      intros xs. set_unfold. intros (x&?&?&?&?). exfalso; edestruct Hinl as (?&?&?); eauto.
    - eapply (set_finite_setoid_quotient (λ xs, match xs with
                                             | [](x, [])
                                             | x' :: tl(x', tl)
                                             end)
                                  _
                                  (setoid_closure {[ ab | fst ab X snd ab Y]}));
      last eapply setoid_closure_pres_fin, set_finite_setoid_product; eauto.
      × intros xs (x0&x1&Hequiv&?&?).
        subst. set_unfold; auto.
        destruct xs as [|x0' x1']; inversion Hequiv; subst.
         (x0, x1); split_and!; eauto.
        econstructor; eauto.
      × intros (x', xs').
         (setoid_closure {[x' :: xs']}). split.
        ** [x' :: xs']. intros xs'' (xin&Hin&?).
           apply elem_of_singleton_1 in Hin; subst. eexists; split; eauto. left.
        ** intros xs'' (x0&x1&Hequiv&?&?). inversion Hequiv; subst. inversion 1; subst. set_unfold.
            (x' :: xs'); split; auto.
           econstructor; eauto.
  Qed.

  Lemma set_finite_refine_cmra_split (x: refine_ucmra K):
    set_finite_setoid {[ ab | (fst ab snd ab) fst ab snd ab x]}.
  Proof.
    eapply (set_finite_setoid_inj _ (λ (ab: refine_cmra K × refine_cmra K),
                                     (validity_car (fst ab), validity_car (snd ab)))).
    - intros (a&b) (a'&b') (Hval&Hmult) (Hequiv1&Hequiv2).
      simpl in ×.
      inversion Hequiv1 as [Hcov1 Hequiv1'].
      inversion Hequiv2 as [Hcov2 Hequiv2'].
      econstructor; simpl; [eapply Hequiv1' | eapply Hequiv2']; eauto.
    - intros (a&b) (a'&b') (Hval1&Hmult1) (Hval2&Hmult2) (Hequiv1&Hequiv2); simpl in ×.
      econstructor; simpl; (econstructor; first split; eauto).
    - eapply set_finite_implies_setoid.
      eapply set_finite_subseteq; last eapply (set_finite_refine_car_split (validity_car x)).
      set_unfold. intros (a&b) (y&Heq&Hval&Hmult).
      rewrite -leibniz_equiv_iff.
      simpl in ×.
      inversion Heq; subst.
      inversion Hmult as [? HequivMult]. rewrite -HequivMult; auto. simpl.
      destruct Hval as (?&?&?); auto.
      split_and!; eauto;
      eapply validity_valid_car_valid; eauto.
  Qed.

  Lemma set_finite_refine_cmra_split_list n (x: refine_cmra K):
    set_finite_setoid {[ xs | (big_op xs) big_op xs x length xs n]}.
  Proof.
    revert x; induction n.
    - intros x. [[]]. intros x' (?&?&?).
       []. destruct x'; simpl in *; last omega.
      split; auto. set_unfold. auto.
    - intros x.
      eapply (set_finite_setoid_quotient
                (λ xs, match xs with
                         | [](, )
                         | x' :: tl(x', big_op tl)
                       end) _ ({[ ab | (fst ab snd ab) fst ab snd ab x]})).
      × intros xs (Hval&Hequiv&Hlen).
         destruct xs as [| x' xs'].
         ** simpl in ×. set_unfold. split; auto. rewrite left_id. auto.
         ** set_unfold. split; auto.
      × intros (a&b).
         ({[[]]} {[ xs | x xs', xs x :: xs' x setoid_closure {[a]}
                                                 xs' {[ xs' | big_op xs'
                                                                   big_op xs' b
                                                                   length xs' n]}]}).
        split.
        ** eapply union_finite_setoid; first apply set_finite_implies_setoid, singleton_finite.
           eapply set_finite_setoid_list_cons; eauto.
           eapply setoid_closure_pres_fin.
           eapply set_finite_implies_setoid, singleton_finite; eauto.
        ** intros xs (Hval&Hmult&Hlen).
           destruct xs as [|x' xs'].
           *** left. set_unfold; auto.
           *** intros (Hequiv1&Hequiv2).
               set_unfold.
               right.
                x', xs'.
               split_and!; eauto.
               omega.
      × eapply set_finite_refine_cmra_split.
  Qed.

  Lemma set_finite_interp_codomain_bigop n (x: refine_cmra K):
    set_finite_setoid {[ xs | big_op (snap_vector xs) x length (snap_vector xs) n]}.
  Proof.
    eapply (set_finite_setoid_inj _ snap_vector).
    - intros x1 x2. set_unfold. intros (?&?).
      auto.
    - intros x1 x2. set_unfold. intros (?&?) (?&?) Hequiv.
      auto.
    - eapply set_finite_setoid_subseteq;
      last eapply (set_finite_refine_cmra_split_list n x).
      set_unfold. intros svs (y&?&?&?). subst. split_and!; auto.
      destruct y. auto.
  Qed.

  Lemma set_finite_le n:
    set_finite {[ n' | n' n]}.
  Proof.
    induction n as [| n].
    - [0]. set_unfold. intros x. left. omega.
    - edestruct IHn as [l Hin_l]. (S n :: l).
      set_unfold. intros x. inversion 1; subst; auto.
  Qed.

  Lemma set_finite_init_idx c ixs:
    set_finite {[ r | r (match cfgs K r with
                      | []False
                      | c' :: _c' = c
                      end) idxs K r = ixs]}.
  Proof.
    destruct (valid_cfg_seq_dec c ixs) as [(cs&Hval)|Hne].
    {
    eapply (set_finite_quotient _ _ (λ r, tids K r)
                                _
                                {[ B | B ns_leq (length (fst c) + length ixs)]}).
    - clear Hval cs.
      intros r.
      set_unfold. intros (Hval&Hinit&Hidxs).
      destruct r as [v ts cs ixs'].
      simpl in ×. subst. destruct cs as [| c' cs']; first (exfalso; auto).
      subst. destruct Hval as [Hbound Hval]. simpl in ×.
      remember (c :: cs') as cs eqn:Hcs.
      revert c cs' Hcs Hbound.
      induction Hval.
      × intros; congruence.
      × intros c' cs'.
        destruct cs' as [|]; last (congruence; done).
        inversion 1; subst.
        simpl. intros Hbound.
        intros n Hin. eapply ns_leq_spec.
        specialize (Hbound _ Hin). omega.
      × intros c'' cs''.
        destruct cs'' as [|]; first (congruence; done).
        injection 1. intros <- <- <-.
        simpl in ×. intros Hrec.
        intros x Hin.
        assert (x ns_leq (length (fst c') + length idxs)) as IHbound.
        { eapply IHHval; eauto. }
        eapply ns_leq_spec in IHbound.
        apply ns_leq_spec.
        assert (S (length (fst c)) length (fst c')) by (eapply length_cfg_idx_step'; eauto).
        omega.
    - intros ts.
       ({[ Refine K snapshot ts (c :: cs) ixs]}
               {[ Refine K master ts (c :: cs) ixs]}).
      split.
      ** eapply union_finite; eapply singleton_finite.
      ** set_unfold. intros r.
         destruct r as [v ts' cs' ixs'].
         simpl. intros (Hval'&Hhd&->).
         destruct cs' as [|c' cs']; first (exfalso; auto).
         subst.
         destruct Hval' as (_&Hval'). simpl in ×.
         assert (cs' = cs) asby (eapply valid_seq_inj2; simpl; eauto).
         intros. assert (ts' = ts) as →. apply mapset_eq. auto.
         destruct v; auto.
    - eapply natset_powerset_finite.
    }
    {
       []. set_unfold. intros r ((_&Hval)&Hb&Hixs) .
      destruct (cfgs K r); auto.
      subst. eapply Hne; eauto.
    }
  Qed.

  Lemma suffix_set_finite A (l: list A):
    set_finite {[ l' | l' `suffix_of` l]}.
  Proof.
    induction l as [| a l] using rev_ind.
    - [[]]. intros l.
      inversion 1 as (lext&Heq).
      symmetry in Heq.
      apply app_eq_nil in Heq as (?&?).
      subst. econstructor.
    - destruct IHl as (L&Hin_L).
       ([] :: (map (λ l', l' ++ [a]) L)).
      intros l'.
      inversion 1 as (lext&Heq).
      destruct l' as [|a' l''] using rev_ind.
      ** left.
      ** rewrite app_assoc in Heq. apply app_inj_2 in Heq as (Heq1&Heq2); auto.
         inversion Heq2; subst.
         right.
         assert (l'' ++ [a'] = (λ l', l' ++ [a']) l'') as Heq; auto.
         eapply (elem_of_map (λ l', l' ++ [a']) _ l'').
         eapply Hin_L.
          lext. eauto.
  Qed.

  Lemma set_finite_app1 {A: Type} (l1 l2: list A):
    set_finite {[ l | l1 ++ l = l2 ]}.
  Proof.
    eapply set_finite_subseteq; last (eapply (suffix_set_finite _ l2)).
    intros l. inversion 1. subst. eexists. eauto.
  Qed.

  Lemma set_finite_app2 {A: Type} (l1: list A) Lext:
    set_finite Lext
    set_finite {[ l2 | l, l Lext l1 ++ l = l2 ]}.
  Proof.
    eapply (set_finite_quotient _ _ (λ l, skipn (length l1) l) _ Lext).
    - intros l. inversion 1 as (l' & Hin & Heq).
      subst. rewrite drop_app. auto.
    - intros l. {[l1 ++ l]}. split; eauto.
      × eapply singleton_finite.
      × intros l'. inversion 1 as (l'' & Hin & Heq).
        subst. rewrite drop_app. intros →. set_solver+.
  Qed.

  Lemma set_finite_powerlist {A: Type} (L: set A) (n: nat):
    set_finite L
    set_finite {[ l' | length l' = n a, a l' a L]}.
  Proof.
    induction n.
    - simpl. [[]]. intros l'. set_unfold. destruct l' as [| ? ?]; simpl; intros; last omega.
      left. auto.
    - intros. eapply (set_finite_subseteq
                {[ l | a l', l = a :: l' a L
                              l' {[ l' | length l' = n ( a: A, a l' a L)]}]}).

      × set_unfold. intros l (Hlen&Hcontents).
        destruct l as [| a l'] ; simpl in *; first omega.
         a, l'.
        split_and!; auto.
        ** eapply Hcontents. left; eauto.
        ** intros. eapply Hcontents; right; auto.
      × eapply set_finite_list_cons; eauto.
  Qed.

  Lemma set_finite_powerlist_upto {A: Type} (L: set A) (n: nat):
    set_finite L
    set_finite {[ l' | length l' n a, a l' a L]}.
  Proof.
    induction n.
    - simpl. [[]]. intros l'. set_unfold. destruct l' as [| ? ?]; simpl; intros; last omega.
      left. auto.
    - intros. eapply (set_finite_subseteq
                ({[[]]} {[ l | a l', l = a :: l' a L
                              l' {[ l' | length l' n ( a: A, a l' a L)]}]})).
      × set_unfold. intros l (Hlen&Hcontents).
        destruct l as [| a l']; first left; auto.
        right.
         a, l'.
        split_and!; auto.
        ** eapply Hcontents. left; eauto.
        ** simpl in ×. omega.
        ** intros. eapply Hcontents; right; auto.
      × eapply union_finite.
        ** apply singleton_finite.
        ** eapply set_finite_list_cons; eauto.
  Qed.

  Lemma set_finite_permutation {A: Type} (l: list A):
    set_finite {[ l' | Permutation l' l]}.
  Proof.
    eapply (set_finite_subseteq ({[ l' | length l' = length l a, a l' a {[ a | a l]}]})).
    - set_unfold. intros l' Hperm; split.
      ** apply Permutation_length; auto.
      ** intros x. rewrite Hperm. auto.
    - apply set_finite_powerlist. l. eauto.
  Qed.

  Lemma idx_step_inv_big n i (rs1 rs2: list (cmra_car (refine_ucmra K))):
    idx_stepN n i rs1 rs2
     r1 r2 rs, r1 _(n) r2 big_op rs1 r1 big_op rs big_op rs2 r2 big_op rs
                 length rs2 S (length rs1)
                ( t1 t2, rs1 = t1 ++ r1 :: t2 length t1 = i).
  Proof.
    inversion 1 as [r r' t1 t2 t1' t2' Heq_pre Heq_post Hstep Hlen Hequiv1 Hequiv2|
                    r r' rf t1 t2 t1' t2' Heq_pre Heq_post Hstep Hlen Hequiv1
                      Hequiv2]; subst.
    - r, r', (t1 ++ t2).
      split_and!; auto; try rewrite ?big_op_app //= Hequiv1 Hequiv2; try solve_equiv'.
      × rewrite //= ?app_length //=. omega.
      × do 2 eexists; split; eauto.
    - r, (r' rf), (t1 ++ t2).
      split_and!; auto; try rewrite ?big_op_app //= Hequiv1 Hequiv2.
      ** solve_equiv'.
      ** rewrite ?big_op_app. simpl. solve_equiv'.
      ** rewrite //= ?app_length //= ?app_length //=. omega.
      ** do 2 eexists; split; eauto.
  Qed.

  Lemma set_finite_setoid_option `{Equiv A, Equivalence A (≡)} (X: set A):
          @set_finite_setoid A _ _ _ X
          @set_finite_setoid (option A) _ _ _
                             {[ mx | match mx with | NoneTrue | Some xx X end ]}.
  Proof.
    intros Hfin.
    eapply (set_finite_setoid_subseteq ({[None]}
       {[ mx | match mx with | NoneFalse | Some xx X end]})).
    - set_unfold. intros [x|]; auto.
    - apply union_finite_setoid.
      × eapply set_finite_implies_setoid, singleton_finite.
      × eapply (set_finite_setoid_quotient_strong id _ X).
        ** intros [x|]; set_unfold.
           *** intros; x; split; auto.
           *** intros; exfalso; auto.
        ** intros x. (setoid_closure {[Some x]}).
           split; first eapply setoid_closure_pres_fin, set_finite_implies_setoid, singleton_finite.
           set_unfold. intros [x'|] Hin Hequiv.
           *** eexists; split; auto.
           *** exfalso; auto.
        ** auto.
  Qed.

  Lemma interp_bounded_idxs_finite n c ixs:
    @set_finite_setoid interp_codomain _ _ _
                       {[ x | match (cfgs K (validity_car (big_op (snap_vector x)))) with
                                | []False
                                | c' :: _c' = c
                              end
                              idxs K (validity_car (big_op (snap_vector x))) ixs
                              length (snap_vector x) n ]}.
  Proof.
    eapply (set_finite_setoid_quotient (λ x, validity_car (big_op (snap_vector x))));
    last (eapply set_finite_implies_setoid, (set_finite_init_idx c ixs)).
    - intros x. set_unfold.
      destruct x as [svx compatx ?]. simpl.
      intros (Hcs&Hixs&Hlen).
      destruct (big_op svx). split_and!; eauto.
      apply leibniz_equiv_iff in Hixs. auto.
    - intros res.
      eexists; split; first (eapply (set_finite_interp_codomain_bigop n (to_validity res))).
      set_unfold. intros x (Hcfgs&Hidxs&Hlen) Hequiv.
      split.
      × inversion Hequiv. subst.
        econstructor; auto.
        split; last (destruct x; auto).
        intros. assert ( validity_car (big_op (snap_vector x))) by (eapply validity_prf; eauto).
        eauto.
      × eauto.
  Qed.

  Instance cfg_equiv : Equiv (cfg ) := (=).
  Instance cfg_equivalence : Equivalence ((≡): relation (cfg )).
  Proof. by split; eauto with ×. Qed.
  Instance cfg_leibniz : LeibnizEquiv (cfg ).
  Proof. by intro. Qed.
  Lemma set_to_natset:
     (S: natset), (S': set nat), set_finite S' n, n S n S'.
  Proof.
    intros S.
     {[ n | n S ]}.
    set_unfold. split.
    assert (set_finite S) as (l&Hin) by eapply fin_collection_finite.
     l. set_unfold; auto.
    auto.
  Qed.
  Lemma fold_left_max_le_acc_irrel:
     l1 x l2 acc,
      x acc
      fold_left max (l1 ++ [x] ++ l2) acc = fold_left max (l1 ++ l2) acc.
  Proof.
    induction l1; simpl; intros.
    - rewrite ?Max.max_l; auto.
    - eapply IHl1. etransitivity; eauto.
      eapply Max.le_max_l.
  Qed.

  Lemma fold_left_max_gt_acc_irrel:
     l1 x l2 acc1 acc2,
      acc1 x acc2 x
      fold_left max (l1 ++ [x] ++ l2) acc1 = fold_left max (l1 ++ [x] ++ l2) acc2.
  Proof.
    induction l1; simpl; intros.
    - rewrite ?Max.max_r; auto.
    - case (decide (a x)).
      × intros Hle. eapply IHl1;
        eauto with ×.
      × intros. assert (x a). omega.
        rewrite ?Max.max_r; omega.
  Qed.
Lemma fold_max_is_last_cfg r:
    r
   default 0 (last (cfgs K (validity_car r))) (length fst) =
   fold_left Init.Nat.max (map (length fst) (cfgs K (validity_car r))) 0.
Proof.
  destruct r as [r Hval Hprf].
  simpl. intros. assert ( r) as [? Hval'] by eauto.
  revert Hval'.
  destruct (cfgs K r) using rev_ind. auto.
  rewrite last_snoc. simpl.
  clear -K_nz. remember (idxs K r) as ixs eqn:Heq. clear Heq.
  revert ixs. induction l. simpl; auto.
  rewrite map_app. simpl.

  idtac. intros ixs Hval.
  rewrite (fold_left_max_gt_acc_irrel _ _ [] (length (fst a)) 0).
  - simpl. rewrite map_app in IHl.
    inversion Hval.
    × exfalso. destruct l; simpl in *; congruence.
    × subst. eapply IHl. rewrite -H0. eauto.
  - eapply valid_seq_tp_monotone_all_tl. rewrite app_comm_cons in Hval. eauto.
    set_solver+.
  - omega.
Qed.

  Lemma interp_step_bounded_nondet_aux x i:
    @set_finite_setoid (option interp_codomain) _ _ _ {[ y | interp_step i x y ]}.
  Proof.
    destruct x as [x|].
    - destruct x as [svx compatx all_snapsx all_nex all_threadsx].
      assert ( c', match (cfgs K (validity_car (big_op svx))) with
                        | []False
                        | chd :: cs'c' = chd
                    end) as (chd&Hhd).
      {
        destruct (cfgs K _); first (congruence; done).
        eexists; eauto.
      }
      pose (curr := (validity_car (big_op svx))).
      eapply (set_finite_setoid_quotient_strong
                (λ my, match my with
                       | NoneNone
                       | Some y
                         match cfgs K (validity_car (big_op (snap_vector y))) with
                         | []None
                         | chd' :: _Some (length (snap_vector y),
                                              chd',
                                              (idxs K (validity_car (big_op (snap_vector y)))))
                         end
                       end)
                _
                ({[ nhl | fst (fst nhl) {[ n | n S (length svx)]}
                          snd (fst nhl) {[chd]}
                          snd nhl {[l2 | l, l {[ l' | length l' K × size (tids K curr)
                                           a, a l' a (tids K curr)]}
                               (idxs K curr) ++ l = l2 ]}]})).
      × intros [y| ]; last (set_unfold; intros; exfalso; auto; done).
        destruct y as [svy compaty all_snapsy all_threadsy].
        set_unfold.
        intros (r1&r1'&rs&Hstep&Hequivsvx&Hequivsvy&Hlen&_)%idx_step_inv_big.
        assert ( (r1 big_op rs)) as Hval_prod.
        { rewrite -Hequivsvx; auto. }
        assert ( (r1' big_op rs)) as Hval_prod'.
        { rewrite -Hequivsvy; auto. }
        destruct Hval_prod as (Hvalr1&Hval_rest&Hdisj).
        destruct Hval_prod' as (Hvalr1'&_&Hdisj').
        assert ( validity_car r1) as Hvalcar by (destruct r1; eauto).
        assert ( validity_car r1') as Hvalcar' by (destruct r1'; eauto).
        assert ( validity_car (big_op rs)) as Hvalcarrest
            by (destruct (big_op rs); eauto).
        assert (tids K (validity_car (big_op svx))
                = tids K (validity_car r1) tids K (validity_car (big_op rs)))
          as Hunion_tids.
        {
          clear -Hequivsvx compatx.
          eapply validity_car_proper in Hequivsvx; eauto.
          simpl in Hequivsvx.
          eapply (tids_proper) in Hequivsvx.
          rewrite /op /cmra_op /dra_op //= /refine_op in Hequivsvx.
          destruct le_dec; simpl in *; auto.
        }
        edestruct (refine_step_disjoint_all_threads' K (validity_car r1)
                                                     (validity_car (big_op rs))
                                                     (validity_car r1'))
        as (cs0&c0&c&csext&isext&Heqcs0&Heqcs&Heqidxs&Hin_isext&Hlen_isext&Hall_new); eauto.
        { inversion Hstep. eauto. }
        { eapply validity_car_proper in Hequivsvx; eauto.
          simpl in Hequivsvx. rewrite -Hequivsvx.
          rewrite fold_max_is_last_cfg; last auto.
          rewrite -Hunion_tids.
          eauto.
        }
         (length svy, chd, idxs K (validity_car (big_op svy))).
        split_and!.
        ** eapply validity_car_proper in Hequivsvx; auto.
            simpl in Hequivsvx.
            eapply cfgs_proper in Hequivsvx.
            rewrite -Hequivsvx in Heqcs.
            eapply validity_car_proper in Hequivsvy; auto.
            simpl in Hequivsvy.
            eapply cfgs_proper in Hequivsvy.
            rewrite Hequivsvy.
            rewrite Heqcs.
            destruct (cfgs K (validity_car (big_op svx))).
            *** exfalso; eapply Hhd.
            *** simpl. congruence.
        ** auto.
        ** simpl. auto.
        ** isext. unfold curr. rewrite Hunion_tids.
           split_and!; auto.
           intros n. clear -Hin_isext. set_solver.
           eapply validity_car_proper in Hequivsvx; auto.
           rewrite Hequivsvx.
           apply validity_car_proper in Hequivsvy; auto.
           rewrite Hequivsvy.
           simpl. auto.
      × intros ((n&c)&ixs).



        eexists; split;
        first (eapply set_finite_setoid_option, (interp_bounded_idxs_finite n c ixs)).
        set_unfold. intros [x|]; last (intros; exfalso; auto; done).
        intros His Hequiv.
        set_unfold.
        destruct (cfgs K (validity_car (big_op (snap_vector x)))).
        ** inversion Hequiv.
        ** inversion Hequiv as [? ? Hequiv'|]; subst.
           inversion Hequiv' as (Hequiv1&Hequiv2).
           simpl in ×. inversion Hequiv1 as (Hequiv1a&Hequiv1b).
           simpl in ×.
           inversion Hequiv1a.
           eapply leibniz_equiv_iff in Hequiv1b.
           split_and!; auto.
      × apply set_finite_implies_setoid.
        eapply set_finite_product3.
        ** eapply set_finite_le.
        ** apply singleton_finite.
        ** eapply set_finite_app2.

           idtac.

           destruct (set_to_natset (tids K curr)) as (S&?&Hspec).
           eapply (set_finite_subseteq
                  ({[ l' | length l' K × size (tids K curr)
                           ( a : nat, a l' a S) ]})).
           { set_unfold. intros ? (?&?); split; eauto.
             intros n. rewrite -Hspec. auto. }
           eapply set_finite_powerlist_upto; auto.
    - []. set_unfold. intros. exfalso. auto.
  Qed.

  Fixpoint step_block_list x n :=
    match n with
    | Onil
    | S n'{[ y | interp_step n' x y]} :: step_block_list x n'
    end.

  Lemma step_block_list_spec x n X :
    X step_block_list x n
       i, i < n X = {[ y | interp_step i x y]}.
  Proof.
    induction n.
    - simpl. split; first set_solver+.
      intros (i&Hlt&?). omega.
    - simpl. split.
      × inversion 1; subst.
        ** n; split; auto.
        ** edestruct IHn as (IHn'&_). edestruct IHn' as (i&?&?); eauto.
      × intros (i&Hlt&Hequiv).
        inversion Hlt; subst.
        ** apply elem_of_cons. left. auto.
        ** right. eapply IHn. eauto.
  Qed.

  Lemma idx_stepN_length {M: cmraT} n i (x y: list M): idx_stepN n i x y i < length x.
  Proof.
    rewrite idx_stepN_equiv. induction 1; simpl; omega.
  Qed.

  Lemma interp_step_bounded_nondet x:
    @set_finite_setoid (option interp_codomain) _ _ _ {[ y | i, interp_step i x y ]}.
  Proof.
    destruct x as [x|].
    - eapply (set_finite_setoid_flatten _ (step_block_list (Some x) (length (snap_vector x)))).
      × intros X'.
        rewrite step_block_list_spec. intros (i'&Hlt&->).
        eapply interp_step_bounded_nondet_aux.
      × set_unfold.
        intros my (i&Hstep). destruct my as [y|]; last (exfalso; auto).
         {[ y | interp_step i (Some x) y]}.
        split.
        ** eapply step_block_list_spec. i; split; auto. eapply idx_stepN_length; eauto.
        ** set_unfold; auto.
    - []. set_unfold. intros ? (n&?). exfalso; auto.
  Qed.

  Lemma sumbool_iff_case `{Equiv A}:
     P Q (decP: {P} + {¬P}) (decQ: {Q} + {¬Q}) C D C' D', P Q
                                                           ( v v', C v C' v')
                                                           ( nv nv', D nv D' nv')
                                                           ((match decP with
                                                             | left vC v
                                                             | right nvD nv
                                                             end) : A)
                                                                       ((match decQ with
                                                                         | left vC' v
                                                                         | right nvD' nv
                                                                         end) : A).
  Proof.
    intros P Q decP decQ C D C' D' Hiff Heqtrue Heqfalse.
    destruct decP as [|n]; destruct decQ as [|n']; auto.
    - exfalso. eapply n'. rewrite -Hiff. eauto.
    - exfalso. eapply n. rewrite Hiff. eauto.
  Qed.

  Lemma eq_sym_involutive {A: Type} {x y: A} (prf: x = y):
    eq_sym (eq_sym prf) = prf.
  Proof.
    destruct prf. simpl. auto.
  Qed.

  Definition gst_refine_update (g: iGst Λ (globalF Σ)) (r: refine_cmra K) : iGst Λ (globalF Σ).
  Proof.
    refine (iprod_insert (@inG_id Λ Σ _ (refine_inG)) _ _).
    apply (ucmra_transport inG_prf r).
    apply g.
  Defined.

  Lemma interp_extract_step_reflect x r n:
    interp_extract x _(n) r
     y, x _(n) y interp_extract y = r.
  Proof.
    intros Hie.
    pose (y := Res (wld x) (pst x) (gst_refine_update (gst x) r) : iRes Λ (globalF Σ)).
     y. split.
    - intros g.
      intros. subst. unfold interp_extract in ×. unfold y.
      simpl.
      unfold gst_refine_update. rewrite /iprod_insert.
      destruct decide; simpl.
      × destruct e. simpl.
        specialize (ucmra_transport_sym_inv (eq_sym (@inG_prf Λ Σ _ (refine_inG)))).
        intros Hfun. specialize (Hfun (gst x (@inG_id Λ Σ _ (refine_inG)))).
        rewrite -Hfun.

        rewrite eq_sym_involutive.
        eapply ucmra_transport_stepN; auto.
      × eapply refine_alt_triv.
        split; eauto.
    - unfold y, interp_extract. simpl.
      unfold gst_refine_update.
      rewrite iprod_lookup_insert.
      rewrite ucmra_transport_sym_inv; auto.
  Qed.


  Lemma view_of_op r1 r2:
    view K (r1 r2) = max_view (view K r1) (view K r2).
  Proof.
    rewrite /op //= /refine_op //=; destruct le_dec; auto.
  Qed.

  Lemma op_snap_iff r1 r2:
    view K r1 = snapshot view K r2 = snapshot view K (r1 r2) = snapshot.
  Proof.
    rewrite view_of_op.
    split.
    - intros (->&->); auto.
    - intros. destruct view; destruct view; auto.
  Qed.

  Lemma bigop_snap_iff (rs: list (refine_cmra K)):
    ( r, r rs view K (validity_car r) = snapshot)
                                                          (view K (validity_car (big_op rs)) = snapshot).
  Proof.
    induction rs as [| r rs].
    - simpl. split; auto. set_solver+.
    - split; simpl.
      × intros Hin.
        idtac. rewrite view_of_op.
        destruct IHrs as [IH _].
        rewrite (Hin r); last set_solver+.
        rewrite IH; auto.
        intros r' Hin'. eapply Hin. clear -Hin'. set_solver.
      × rewrite view_of_op.
        intros Hmax_view r' [Hr|Hrs]%elem_of_cons.
        ** subst. destruct (view K (validity_car r)); auto.
        ** eapply IHrs; auto.
           destruct (view K (validity_car (big_op rs))); auto.
           destruct view; simpl in *; congruence.
  Qed.

  Lemma interp_some n rs:
    ✓{n} big_op (map interp_extract rs)
    ( r, r (map interp_extract rs)
          view K (validity_car r) = snapshot)
    (cfgs K (validity_car (big_op (map interp_extract rs))) [])
    ( i : nat,
        i <
        fold_left Init.Nat.max
                  (map (length fst)
                       (cfgs K (validity_car (big_op (map interp_extract rs))))) 0
                   i tids K (validity_car (big_op (map interp_extract rs))))
    interp n rs None.
  Proof.
    intros Hcompat Hallsnap Hne Hallts.
    unfold interp.
    destruct excluded_middle_informative as [|Hn];
      last (exfalso; eapply Hn; eauto; done).
    destruct excluded_middle_informative as [|Hn];
      last (exfalso; eapply Hn; eauto; done).
    destruct excluded_middle_informative as [|Hn];
      last (exfalso; eapply Hn; eauto; done).
    destruct decide as [|Hn];
      last (exfalso; eapply Hn; eauto; done).
    auto.
  Qed.

  Lemma idx_stepN_map_extract n i robs robs':
    idx_stepN (S n) i robs robs'
    idx_stepN (S n) i (map interp_extract robs) (map interp_extract robs').
  Proof.
    inversion 1; subst.
    - rewrite ?map_app; simpl.
      econstructor; eauto.
      × eapply interp_extract_stepN; auto.
      × apply map_length.
      × apply map_proper; auto. apply interp_extract_proper.
      × apply map_proper; auto. apply interp_extract_proper.
    - rewrite ?map_app //= ?map_app; simpl.
      eapply idx_stepN_fork; eauto.
      × rewrite -interp_extract_op. eapply interp_extract_stepN; auto.
      × apply map_length.
      × apply map_proper; auto. apply interp_extract_proper.
      × apply map_proper; auto. apply interp_extract_proper.
  Qed.

  Lemma interp_not_none_inv:
     n rs, interp n rs None x, interp n rs = Some x.
  Proof.
    intros n rs; destruct (interp n rs).
    - eexists; eauto.
    - congruence.
  Qed.

  Lemma interp_some_inv:
     n rs x, interp n rs = Some x snap_vector x = map (interp_extract) rs.
  Proof.
    intros n rs x; unfold interp.
    repeat destruct excluded_middle_informative; try (congruence); [|];
    repeat destruct decide; try (congruence); [].
    inversion 1. subst. auto.
  Qed.

  Lemma big_op_tids_split (rs: list (refine_cmra K)) (i: nat):
    i (tids K (validity_car (big_op rs)))
     t1 t2 r n, rs = t1 ++ r :: t2
                 length t1 = n
                 i tids K (validity_car r).
  Proof.
    revert i. induction rs as [| r rs].
    - simpl. set_solver+.
    - simpl. intros i Hin.
      assert (tids K (validity_car r validity_car (big_op rs))
              = tids K (validity_car r) tids K (validity_car (big_op rs)))
        as Hunion_tids.
      {
        rewrite /op /cmra_op /refine_op.
        destruct le_dec; simpl in *; auto.
      }
      rewrite Hunion_tids in Hin.
      apply elem_of_union in Hin as [Hin1|Hinrest].
      × [], rs, r, 0.
        split_and!; auto.
      × edestruct (IHrs i) as (t1&t2&r'&n&Heq1&Hlen&Hin); auto; auto.
         (r :: t1), t2, r', (S n).
        split_and!; subst; auto.
  Qed.

  Definition ht_adequacy_own_inf_hom2_alt Λ Σ B B_idx_step F phiob phi e
             sigma tr m1 m2 n prf1 prf2 prf3 prf4 prf5 prf6 prf7 :=
    @ht_adequacy_own_inf_hom2 Λ Σ B B_idx_step F prf1 prf2 prf3 prf4 prf5 prf6 prf7
                              phiob phi e sigma tr m1 m2 n.


  Lemma step_block_or_none_enabled (c: cfg ) (ts: natset):
    ( cs c' idxs, valid_cfg_idx_seq ([c] ++ cs ++ [c']) idxs
                   ( i, i ts (i idxs ¬ (enabled idx_step c' i)))
                   ( i, i ts (count_occ (nat_eq_dec) idxs i K))
                   ( i, i idxs i ts))
    ( j, j ts ¬ enabled idx_step c j).
  Proof.
    remember (size ts) as n eqn:Hsize.
    assert (size ts n) as Hle by omega. clear Hsize.
    revert c ts Hle.
    induction n as [| n].
    - intros c ts Hsize. right.
      assert (ts = ).
      {
        rewrite -leibniz_equiv_iff.
        apply size_empty_iff; auto.
        omega.
      }
      subst. set_solver+.
    - intros c ts Hsize.
      assert (( i, i ts enabled idx_step c i) j, j ts ¬ enabled idx_step c j) as Htry.
      {
        clear -PrimDec. revert ts. eapply collection_ind.
        × intros ts1 ts2 Hequiv.
           split; intros [(i&Hin&?Henabled)|Hnin].
           ** left. i; split; auto; rewrite -Hequiv; auto.
           ** right; intros j Hin; eapply Hnin; rewrite Hequiv; auto.
           ** left. i; split; auto; rewrite Hequiv; auto.
           ** right; intros j Hin; eapply Hnin; rewrite -Hequiv; auto.
        × right. set_solver+.
        × intros i ts Hfresh [(i'&?&?)|Hnone].
          ** left. i'; split; auto; set_solver.
          ** destruct (idx_step_dec' c i) as [(c'&Hstep)|Hnenabled].
             *** left. i. split; first set_solver.
                  c'; eauto.
             *** right. intros j. set_unfold.
                 intros [->|Hin]; auto.
      }
      destruct Htry as [(i&Hin&Henabled)|Hnone]; last auto.
      destruct Henabled as (c'&Hstep).
      destruct (IHn c' (difference ts {[ i ]})) as
          [(cs&c''&ixs&Hval&Hall_enabled&Hmax&Hin_ts)|Hnone_more].
      {
        assert (size (difference ts {[i]}) < size ts).
        { apply subset_size. set_unfold.
          split.
          - intros x (?&?). auto.
          - intros Hfalse. specialize (Hfalse i).
            destruct Hfalse as [? Hfalse]; eauto.
        }
        omega.
      }
      × left. (c' :: cs), c'', (i :: ixs).
        split_and!.
        ** simpl in ×. econstructor; eauto.
        ** set_unfold. intros j Hin'.
           case (decide (j = i)).
           *** intros →. left; auto.
           *** intros Hneq. destruct (Hall_enabled j); auto.
        ** intros j Hin'.
           simpl. destruct nat_eq_dec as [->|Hneq].
           *** assert (count_occ nat_eq_dec ixs j = 0) as →.
               { apply count_occ_not_In.
                 clear -Hin_ts.
                 intros Hin%elem_of_In.
                 specialize (Hin_ts j Hin).
                 set_solver.
               }
               auto.
               clear -K_nz. intros; destruct K; first exfalso; auto.
               omega.
           *** eapply Hmax. clear -Hneq Hin'. set_solver.
        ** intros i' [->|Hin']%elem_of_cons; auto.
           specialize (Hin_ts i' Hin'). clear -Hin_ts. set_solver.
      × left. [], c', [i].
        split_and!.
        ** simpl. econstructor; auto. econstructor.
        ** set_unfold. intros i' Hin'.
           case (decide (i' = i)) as [->|]; auto.
        ** intros i' Hin'. simpl. destruct nat_eq_dec; auto.
           clear -K_nz. intros; destruct K; first exfalso; auto.
           omega.
           omega.
        ** set_unfold. clear -Hin. set_solver.
  Qed.

  Lemma operand_prefix_of_valid_seq:
     (r1 r2: refine_cmra K), (r1 r2)
                                 prefix_of_valid_seq (tids K (validity_car r1))
                                                     (cfgs K (validity_car r1))
                                                     (idxs K (validity_car r1))
                                                     (cfgs K (validity_car (r1 r2)))
                                                     (idxs K (validity_car (r1 r2))).
  Proof.
    intros r1 r2 (Hval1&Hval2&Hdisj).
    assert ( validity_car r1) as Hvcr1 by (destruct r1; auto).
    assert ( validity_car r2) as Hvcr2 by (destruct r2; auto).
    inversion Hdisj.
    - simpl.
      edestruct (prefix_of_valid_seq_op K (validity_car r1) (validity_car r2))
        as [(Hprefix&Hop)|(Hprefix&Hop)]; eauto.
      { rewrite -?H -?H0; simpl; eauto. }
      destruct Hvcr1; auto.
      destruct Hvcr2; auto.
      rewrite Hop. simpl. auto.
      rewrite -?H -?H0 //= in Hprefix ×.
      rewrite Hop. simpl. auto.
      rewrite -?H -?H0 //= in Hprefix ×.
      econstructor; eauto.
       []. split; rewrite ?app_nil_r. auto.
      set_solver+.
    - simpl. rewrite -H -H0.
      rewrite prefix_of_op. simpl.
      econstructor. eexists; eauto.
       is2; split; auto.
      simpl. eexists; eauto.
    - simpl. rewrite -H -H0.
      rewrite prefix_of_op'''; simpl.
      × econstructor; auto. []; rewrite ?app_nil_r; auto; set_solver+.
      × rewrite -H0 in Hvcr2. destruct Hvcr2; auto.
      × rewrite -H in Hvcr1. destruct Hvcr1; auto.
      × eexists; eauto.
      × eexists; eauto.
  Qed.

  Definition ns_between (nle ngt: nat) :=
    match nat_eq_dec nle ngt with
    | left _
    | right _(difference (ns_leq (ngt)) ((ns_leq (nle) {[ngt]}))) {[nle]}
    end.

  Lemma ns_between_spec (nle ngt: nat): nle ngt
                                         n', (n' < ngt nle n') n' ns_between nle ngt.
  Proof.
    intros Hle. unfold ns_between. set_unfold.
    destruct (nat_eq_dec nle ngt).
    - subst. set_unfold. intros. omega.
    - intros n'; split; set_unfold.
      × intros (Hlt & Hgt).
        rewrite -?ns_leq_spec. omega.
      × rewrite -?ns_leq_spec. intros.
        destruct H; omega.
  Qed.

  Lemma step_block_interp_codomain (x: interp_codomain) cs c ts t1 t2 (r: refine_cmra K) n:
    cfgs K (validity_car (big_op (snap_vector x))) = cs ++ [c]
    ( cs c' idxs, valid_cfg_idx_seq ([c] ++ cs ++ [c']) idxs
                   ( i, i ts (i idxs ¬ (enabled idx_step c' i)))
                   ( i, i ts (count_occ (nat_eq_dec) idxs i K))
                   ( i, i idxs i ts))
    snap_vector x = t1 ++ r :: t2
    length t1 = n
    ts = tids K (validity_car r)
    enabled interp_step' x n.
  Proof.
    intros Hcs (cs'&c'&idxs'&Hvalc&Hall_enabled&Hocc&Hin) Hsnap_vector Hlen Hts.
    assert ( cs0 c0 idxs0,
               validity_car r = Refine K snapshot ts (cs0 ++ [c0]) idxs0)
      as (cs0&c0&idxs0&Heq_r).
    { assert ( r) as Hval.
      { destruct x as [svx Hcompatx ? ? ?].
        simpl in ×. eapply elem_of_big_op_valid.
        eauto. rewrite Hsnap_vector. set_solver+.
      }
      assert (view K (validity_car r) = snapshot) as Hr_snap.
      {
        destruct x as [svx ? Hall_snaps ? ?].
        eapply Hall_snaps. simpl in ×. rewrite Hsnap_vector.
        set_solver+.
      }
      destruct r. simpl in ×. assert ( validity_car) as Hvc by auto.
      destruct validity_car as [v1 ts1 cs1 ixs1].
      simpl in ×. destruct cs1 as [| c0 cs0] using rev_ind.
      - destruct Hvc as [Hlt _]. simpl in ×.
        inversion Hvalc as [| | ? ? ? i];
          subst; first (destruct cs'; simpl in *; congruence; done).
        assert (i ts1) by (eapply Hin; set_solver+).
        set_solver.
      - cs0, c0, ixs1. f_equal; auto.
    }
    assert ( r) as Hv_r.
    {
      destruct x as [svx Hcompatx ? ? ?]; simpl; auto.
      simpl in ×.
      eapply (elem_of_big_op_valid _ r) in Hcompatx; first (destruct r; auto).
      rewrite Hsnap_vector. set_solver+.
    }
    assert ( (big_op (t1 ++ t2))) as Hv_12.
    {
      destruct x as [svx Hcompatx ? ? ?]; simpl; auto.
      simpl in ×.
      rewrite big_op_app. auto.
      rewrite Hsnap_vector in Hcompatx.
      rewrite ?big_op_app //= in Hcompatx *; auto.
    }
    assert ( validity_car r) as Hvc_r.
    {
      destruct r; auto.
    }
    assert ( (validity_car (big_op (t1 ++ t2)))) as Hvc_12.
    {
      destruct (big_op (t1 ++ t2)); auto.
    }
    assert ( validity_car (big_op (snap_vector x))) as Hvc_svx.
    {
      destruct x as [svx Hcompatx ? ? ?]; simpl; auto. clear -Hcompatx.
      destruct (big_op svx); auto.
    }
    
    assert ( cspec ispec, valid_cfg_idx_seq ([c0] ++ cspec) ispec
                           cs0 ++ [c0] ++ cspec = cs ++ [c]
                           idxs0 ++ ispec = idxs K (validity_car (big_op (snap_vector x)))
                           ( i, i ispec i ts)) as (cspec&ispec&Hval_spec&Heq_cs_spec
                                                          &Heq_is_spec&Hin_spec).
    {
      
      
      edestruct (operand_prefix_of_valid_seq r (big_op (t1 ++ t2))) as (Hcs_prefix&His_prefix).
      {
        destruct x as [svx Hcompatx ? ? ?].
        simpl in ×. rewrite Hsnap_vector in Hcompatx.
        rewrite ?big_op_app in Hcompatx ×. simpl. auto.
      }
      destruct Hvc_svx as [? Hval_cfg_svx].
      destruct Hvc_r as [? Hval_cfg_r].
      assert (validity_car (r (big_op (t1 ++ t2)))
                           validity_car (big_op (snap_vector x))) as Hvc_equiv.
      {
        symmetry. destruct x as [svx Hcompatx ? ? ?]. eapply validity_car_proper; auto.
        simpl in ×. rewrite Hsnap_vector.
        rewrite ?big_op_app //=. rewrite ?assoc.
        rewrite (comm _ r). auto.
      }
      rewrite Hvc_equiv in Hcs_prefix ×.
      rewrite Hcs. intros (cspec&Heq_cspec).
      rewrite Heq_r //= in Heq_cspec.
      rewrite Hvc_equiv in His_prefix ×.
      destruct (His_prefix) as (ispec&Heq_ispec&Hnin).
       cspec, ispec. split_and!; auto.
      rewrite Hcs in Hval_cfg_svx.
      rewrite Heq_cspec in Hval_cfg_svx.
      rewrite Heq_ispec in Hval_cfg_svx.
      rewrite -assoc in Hval_cfg_svx.
      eapply valid_seq_split; eauto.
      rewrite Heq_r. simpl.
      eapply valid_cfg_idx_length4.
      rewrite Heq_r in Hval_cfg_r. simpl in ×. eauto.
      rewrite assoc. auto.
      rewrite Heq_ispec. rewrite Heq_r. auto.
      clear PrimDet PrimDec.
      set_solver.
    }
    
    assert (validity_car r validity_car (big_op (t1 ++ t2))) as Hdisj_r_12. {
      cut ( (r (big_op (t1 ++ t2)))).
      {
        inversion 1 as (?&?&?). auto.
      }
      destruct x as [svx Hcompatx ? ? ?].
      simpl in ×. rewrite Hsnap_vector in Hcompatx. rewrite ?big_op_app //= in Hcompatx ×.
      auto.
    }
    
    
    pose (r'_vc := Refine K snapshot (ts (ns_between (length (fst c))
                                                          (length (fst c'))))
                          (cs ++ [c] ++ cs' ++ [c'])
                          (idxs K (validity_car (big_op (snap_vector x)))
                                ++ idxs')).
    pose (r':= ((to_validity r'_vc) : refine_cmra K)).
    assert (validity_car r r'_vc).
    {
      rewrite Heq_r.
      eapply snap_spec_step; eauto.
      rewrite Heq_cs_spec. rewrite Heq_is_spec.
      eapply snap_block_step; eauto.
      intros i.
      rewrite -ns_between_spec. omega.
      eapply valid_seq_tp_monotone_all_tl; eauto.
      rewrite assoc in Hvalc. eauto. set_solver+.
    }
    assert (valid_cfg_idx_seq (cs ++ [c] ++ cs' ++ [c'])
                              (idxs K (validity_car (big_op (snap_vector x))) ++ idxs'))
      as Hval_cfg_r'.
    {
      eapply valid_seq_join; eauto. rewrite -Hcs.
      destruct Hvc_svx. auto.
    }
    assert ( r').
    {
      econstructor; eauto.
      assert (length (fst c0) length (fst c')).
      { eapply valid_seq_tp_monotone_all_tl. rewrite ?app_assoc in Hval_cfg_r'.
        eauto.
        rewrite -Heq_cs_spec.
        set_solver+.
      }
      unfold r'_vc. simpl.
      rewrite app_comm_cons.
      rewrite ?app_assoc.
      rewrite last_snoc.
      destruct Hvc_r as [Hts_max ?].
      rewrite Heq_r in Hts_max. simpl in Hts_max. rewrite last_snoc in Hts_max.
      intros i [Hin_ts|Hin_between]%elem_of_union.
      × specialize (Hts_max i Hin_ts). omega.
      × rewrite -ns_between_spec in Hin_between ×. omega.
        eapply valid_seq_tp_monotone_all_tl. rewrite app_assoc in Hvalc.
        eauto.
        set_solver+.
    }
    assert (r _(1) r').
    {
      econstructor.
      split; eauto.
      intros; eauto.
    }
    assert ( y, snap_vector y = t1 ++ r' :: t2) as (y&Hsvy).
    {
      assert (validity_car (big_op (snap_vector x)) = validity_car (r big_op (t1 ++ t2)))
        as Hvc_equiv.
      {
        rewrite -leibniz_equiv_iff.
        eapply validity_car_proper; first (destruct x; simpl in *; auto).
        rewrite Hsnap_vector. rewrite ?big_op_app //= ?assoc (comm _ r); auto.
      }
      assert (validity_car (big_op (snap_vector x)) = validity_car (big_op (t1 ++ t2) r))
        as Hvc_equiv'.
      {
        rewrite -leibniz_equiv_iff.
        eapply validity_car_proper; first (destruct x; simpl in *; auto).
        rewrite Hsnap_vector. rewrite ?big_op_app //= ?assoc -(comm _ r); auto.
        rewrite -(comm _ r). rewrite -assoc. auto.
      }
      assert (cfgs K (validity_car (big_op (t1 ++ t2))) `prefix_of` (cs ++ [c])) as
          Hcs12_prefix.
      {
        rewrite -Hcs.
        rewrite Hvc_equiv'. eapply refine_disjoint_prefix_cfgs_post.
        destruct (big_op (t1 ++ t2)); auto.
        auto.
        symmetry. auto.
      }
      assert ( big_op (t1 ++ r' :: t2)) as Hcompaty.
      { rewrite big_op_app. simpl.
         rewrite assoc. rewrite -(comm _ r').
         rewrite -assoc.
         rewrite -big_op_app.
         split_and!; auto.
         - case_eq (validity_car (big_op (t1 ++ t2))).
           intros v12 ts12 cfgs12 idxs12 Heq_12.
           assert (view K (validity_car (big_op (t1 ++ t2))) = snapshot) as Hview12_snap.
           { simpl.
             apply bigop_snap_iff.
             destruct x as [svx ? Hall_snaps ? ? ].
             simpl in ×. rewrite Hsnap_vector in Hall_snaps.
             intros r0 Hin_r0. apply Hall_snaps.
             clear PrimDet PrimDec.
             set_solver.
           }
           
           rewrite Heq_12 in Hview12_snap. simpl in Hview12_snap.
           subst. simpl. unfold r'_vc.
           idtac.
           destruct Hcs12_prefix as (csext12&Heq_csext12).
           assert (prefix_of_valid_seq (tids K (validity_car (big_op (t1 ++ t2))))
                                       (cfgs K (validity_car (big_op (t1 ++ t2))))
                                       (idxs K (validity_car (big_op (t1 ++ t2))))
                                       (cs ++ [c])
                                       ((idxs K (validity_car (big_op (snap_vector x))))))
             as Hprefix.
           {
             rewrite -Hcs.
             rewrite Hvc_equiv'. eapply refine_disjoint_prefix_of_valid_idxs_post.
             destruct (big_op (t1 ++ t2)); auto.
             auto.
             symmetry. auto.
           }
           Lemma disj_implies_inter_tids_empty:
              r1 r2, r1 r2 tids K r1 tids K r2 .
           Proof.
             inversion 1; simpl; auto.
             rewrite comm; auto.
           Qed.
           idtac.
           assert (tids K (validity_car r) tids K (validity_car (big_op (t1 ++ t2)))
                         ) as Hinter.
           {eapply disj_implies_inter_tids_empty. auto. }
           rewrite Heq_12.
           constructor; eauto.
           × set_unfold.
             intros i ([Hinr|Hinbetween]&Hin12).
             ** rewrite Heq_12 in Hinter. simpl in ×. clear PrimDet. set_solver.
             **
               
               destruct Hvc_12 as [Hmax_ts Hval_cfg_12].
               rewrite -ns_between_spec in Hinbetween *; last first.
               {
                 eapply valid_seq_tp_monotone_all_tl.
                 eauto. rewrite app_comm_cons ?app_assoc in Hval_cfg_r'.
                 eauto. set_solver+.
               }
               
               destruct (cfgs K (validity_car (big_op (t1 ++ t2)))) as [| c12 cs12 _] using
                                                                                         rev_ind.
               *** simpl in Hmax_ts. rewrite Heq_12 in Hmax_ts.
                    clear -Hin12 Hmax_ts. set_solver.
               *** rewrite last_snoc in Hmax_ts.
                    rewrite Heq_12 in Hmax_ts.
                    simpl in ×. assert (length (fst (c12)) length (fst c)).
                    destruct Hvc_svx as [? Hval_cfg_svx].
                    rewrite Hcs in Hval_cfg_svx.
                    eapply valid_seq_tp_monotone_all_tl; eauto.
                    rewrite Heq_csext12. set_solver+.
                    specialize (Hmax_ts i Hin12). omega.
           × right.
             econstructor.
             ** rewrite Heq_12 in Heq_csext12.
                simpl in Heq_csext12.
                 (csext12 ++ cs' ++ [c']).
                rewrite ?app_assoc.
                rewrite Heq_csext12. auto.
             ** destruct Hprefix as (_&isext1&Heq_isext1&Hnin).
                rewrite Heq_isext1.
                rewrite Heq_12. simpl.
                 (isext1 ++ idxs').
                rewrite assoc. split; auto.
                intros i Hin12. rewrite Heq_12 in Hnin Hinter. simpl in Hnin, Hinter.
                clear -Hinter Hnin Hin Hin12.
                intros [Hin_ext1|Hin_idxs']%elem_of_app.
                *** set_solver.
                *** set_solver.
      }
      assert ( r, r t1 ++ r' :: t2 view K (validity_car r) = snapshot) as all_snapsy.
      {
        clear PrimDet.
        destruct x as [svx ? all_snapsx ? ?].
        simpl in ×.
        intros rc. intros [Hin1|Hintl]%elem_of_app.
        - set_solver.
        - eapply elem_of_cons in Hintl as [Hr'|Hin2].
          × subst. auto.
          × set_solver.
      }
      assert (cfgs K (validity_car (big_op (t1 ++ r' :: t2))) =
              cs ++ [c] ++ cs' ++ [c']) as all_cfgsy.
      {
        assert (validity_car (big_op (t1 ++ r' :: t2)) =
                validity_car (r' big_op (t1 ++ t2))) as Hvc_svy.
        {
          rewrite -leibniz_equiv_iff.
          eapply validity_car_proper; auto.
          rewrite ?big_op_app //= ?assoc (comm _ r'); auto.
        }
        rewrite Hvc_svy. simpl. rewrite cfgs_of_prefix_of_op_l; auto.
        etransitivity; first apply Hcs12_prefix.
        simpl. (cs' ++ [c']). rewrite -assoc. simpl. auto.
      }
      assert (cfgs K (validity_car (big_op (t1 ++ r' :: t2))) []) as all_ney.
      {
        rewrite all_cfgsy. destruct cs; simpl in *; congruence.
      }
      Lemma tids_op (r1 r2: refine_cmra K):
        (tids K (validity_car r1 validity_car r2)
         = tids K (validity_car r1) tids K (validity_car r2)).
      Proof.
        rewrite /op /refine_op. simpl. destruct le_dec; auto.
      Qed.

      Lemma tids_op2 (r1 r2: refine_cmra K):
        (tids K (validity_car (r1 r2))
         = tids K (validity_car r1) tids K (validity_car r2)).
      Proof.
        rewrite /op /cmra_op //= /refine_op. eapply tids_op.
      Qed.
      assert ( i, i < fold_left max (map (length fst)
                                          (cfgs K (validity_car (big_op (t1 ++ r' :: t2))))) 0
                                  i tids K (validity_car (big_op (t1 ++ r' :: t2)))) as all_threadsy.
      {
        assert (tids K (validity_car (big_op (snap_vector x))) =
                ts tids K (validity_car (big_op (t1 ++ t2)))) as Htids_x.
        {
          erewrite tids_proper; last first.
          eapply validity_car_proper; first (destruct x; auto).
          rewrite Hsnap_vector. rewrite big_op_app. simpl.
          rewrite assoc. rewrite -(comm _ r). rewrite -assoc -big_op_app.
          reflexivity.
          rewrite tids_op2. rewrite Heq_r. simpl. auto.
        }
        
        assert (tids K (validity_car (big_op (t1 ++ r' :: t2))) =
                ns_between (length (c.1)) (length (c'.1))
                           tids K (validity_car (big_op (snap_vector x)))) as Htids_y.
        {
          erewrite tids_proper; last first.
          eapply validity_car_proper; first auto.
          rewrite big_op_app. simpl. rewrite assoc. rewrite -(comm _ r').
          rewrite -assoc. rewrite -big_op_app. reflexivity.

          rewrite tids_op2. simpl.
          rewrite Htids_x. rewrite -leibniz_equiv_iff. rewrite assoc.
          rewrite (comm _ ts). auto.
        }
        rewrite Htids_y.
        rewrite -fold_max_is_last_cfg; auto.
        rewrite all_cfgsy. simpl. rewrite app_comm_cons assoc. rewrite last_snoc.
        simpl.

        destruct x as [svx ? ? ? all_threadsx].
        simpl in ×.
        rewrite -fold_max_is_last_cfg in all_threadsx; auto.
        rewrite Hcs in all_threadsx.
        rewrite last_snoc in all_threadsx. simpl in ×.
        assert (length (fst c) length (fst c')) as Hlen_le.
        { eapply valid_seq_tp_monotone_all_tl.
          rewrite app_comm_cons in Hval_cfg_r'.
          rewrite assoc in Hval_cfg_r'. eauto.
          set_solver+.
        }
        intros i. set_unfold.
        rewrite -ns_between_spec; auto.
        clear -all_threadsx Hlen_le.
        split.
        - intros. case (decide (i < (length (fst c)))).
          × intros. right. eapply all_threadsx; eauto.
          × intros. left. omega.
        - intros [Hbound|Hin_svx].
          × omega.
          × specialize (proj2 (all_threadsx i) Hin_svx).
            omega.
      }
       ({| snap_vector := t1 ++ r' :: t2;
                 compatible := Hcompaty;
                 all_snaps := all_snapsy;
                 all_ne := all_ney;
                 all_threads := all_threadsy |}).
      simpl. auto.
    }
    
    
     y. econstructor; eauto.
  Qed.


  Lemma map_compose {A B C: Type} (f: A B) (g: B C) (l: list A):
    map (g f) l = map g (map f l).
  Proof.
    induction l; auto.
    simpl. rewrite IHl; auto.
  Qed.

  Lemma map_tids_vc (rs rs': list (refine_cmra K)):
    ( big_op rs)
    rs rs'
    map (tids K validity_car) rs =
    map (tids K validity_car) rs'.
  Proof.
    revert rs'.
    induction rs.
    - simpl. inversion 2. subst. auto.
    - simpl. inversion 2. subst. simpl.
      f_equal; eauto.
      eapply tids_proper. eapply validity_car_proper; eauto.
  Qed.

  Lemma fair_pres_trans {A B C: Type} (R1: nat relation A) (R2: nat relation B)
        (R3: nat relation C) a b c (tr1: trace R1 a) (tr2: trace R2 b) (tr3: trace R3 c):
    fair_pres _ _ tr1 tr2 fair_pres _ _ tr2 tr3 fair_pres _ _ tr1 tr3.
  Proof.
    unfold fair_pres. clear. naive_solver.
  Qed.

  Definition flatten_fair_pres_alt {A R1 B} flatten {a: A} (x: trace R1 a) (R2: nat relation B)
             prf1 prf2 prf3 prf4 prf5 :=
    @flatten_fair_pres A R1 B R2 flatten prf1 prf2 prf3 prf4 prf5 a x.

  Lemma master_snapshot_valid E sσ:
    (to_globalFe (refine snapshot {[0]} [([E], sσ)] [])
       to_globalFe (refine master [([E], sσ)] [])).
  Proof.
    unfold to_globalFe.
      intros i. case (decide (i = (@inG_id Λ Σ _ (refine_inG)))).
      × intros →. rewrite iprod_lookup_op.
        rewrite ?iprod_lookup_singleton.
        rewrite -ucmra_transport_op.
        rewrite ucmra_transport_valid. split_and!.
        ** econstructor.
           *** simpl. set_unfold. intros; omega.
           *** simpl. econstructor.
        ** econstructor.
           *** simpl. set_unfold. intros; omega.
           *** simpl. econstructor.
        ** simpl.
           replace (@nil nat) with (@nil nat ++ @nil nat) at 2; last auto.
           replace ([([E], sσ)]) with ([([E], sσ)] ++ []) at 2; last auto.
           econstructor.
           *** set_solver.
           *** set_solver.
      × intros Hne. rewrite iprod_lookup_op. rewrite ?iprod_lookup_singleton_ne; auto.
        rewrite right_id. eapply ucmra_unit_valid.
  Qed.

      Lemma allts_step_pres (rs rs': list (iRes Λ (globalF Σ))) i n:
        ✓{S n} big_op rs
        ✓{S n} big_op rs'
        idx_stepN (S n) i rs rs'
        view K (validity_car (big_op (map interp_extract rs))) = snapshot
        ( i : nat, i < fold_left Init.Nat.max
                                  (map (length fst) (cfgs K (validity_car
                                               (big_op (map interp_extract rs))))) 0
                                   i tids K (validity_car (big_op (map interp_extract rs))))
        view K (validity_car (big_op (map interp_extract rs'))) = snapshot
        ( i : nat, i < fold_left Init.Nat.max
                                  (map (length fst) (cfgs K (validity_car
                                               (big_op (map interp_extract rs'))))) 0
                                   i tids K (validity_car (big_op (map interp_extract rs'))))
       cfgs K (validity_car (big_op (map interp_extract rs))) `prefix_of`
             cfgs K (validity_car (big_op (map interp_extract rs'))).
      Proof.
        intros Hval Hval' Histep Hallsnap Hallts.
        eapply idx_stepN_map_extract in Histep.
        eapply idx_step_inv_big in Histep as (r1&r2&rs_alt&Hstep&Heq1&Heq2&Hlen).
      inversion Hstep as [Hcov Hcar_step].
      assert ( r1 r2 validity_car r1 validity_car (big_op rs_alt)
               validity_car r2
               validity_car r1 validity_car (big_op rs_alt)) as
          (Hvalr1&Hvalr2&Hvalcr1&Hvalcrs&Hvalcr2&Hdisj).
      {
        apply interp_extract_validN in Hval.
        rewrite interp_extract_bigop in Hval ×.
        rewrite Heq1. inversion 1 as (?&?&?); auto.
        split_and!.
        - auto.
        - eapply Hcov; eauto.
        - destruct r1; eauto.
        - destruct (big_op rs_alt); eauto.
        - assert ( r2). apply Hcov. eauto. destruct r2; auto.
        - auto.
      }
      assert (tids K (validity_car (big_op (map interp_extract rs)))
              = tids K (validity_car r1) tids K (validity_car (big_op rs_alt)))
        as Hunion_tids.
      {
        eapply validity_car_proper in Heq1; eauto.
        simpl in Heq1.
        eapply (tids_proper) in Heq1.
        rewrite /op /cmra_op /dra_op //= /refine_op in Heq1.
        destruct le_dec; simpl in *; auto.
        eapply interp_extract_bigop; auto.
        eapply interp_extract_validN; eauto.
      }
      specialize (Hcar_step Hvalr1).
      edestruct (refine_step_disjoint_all_threads' K (validity_car r1)
                                                   (validity_car (big_op rs_alt))
                                                   (validity_car r2))
        as (_&_&c'&csext&isext&_&Heqcs&_&_&_&Hall&_); eauto.
      {
        apply interp_extract_validN in Hval'.
        rewrite interp_extract_bigop in Hval' ×.
        rewrite Heq2. inversion 1 as (?&?&?); auto.
      }
      {
        generalize Hallts.
        rewrite -fold_max_is_last_cfg.
        intros allts'. intros i'.
        rewrite Hunion_tids in allts'.
        rewrite -(allts' i').
        apply validity_car_proper in Heq1; auto.
        rewrite Heq1. simpl. auto.
        eapply interp_extract_bigop; auto.
        eapply interp_extract_validN; eauto.
        eapply interp_extract_bigop; auto.
        eapply interp_extract_validN; eauto.
      }
      
      
      assert ( big_op (map interp_extract rs)).
      {
        rewrite -interp_extract_bigop. eapply interp_extract_validN; auto.
        eauto.
      }
      assert ( big_op (map interp_extract rs')).
      {
        rewrite -interp_extract_bigop. eapply interp_extract_validN; auto.
        eauto.
      }
      
      
        
        assert (tids K (validity_car (big_op (map interp_extract rs')))
                = tids K (validity_car r2) tids K (validity_car (big_op rs_alt)))
          as Hunion_tids'.
        {
          eapply validity_car_proper in Heq2; eauto.
          simpl in Heq2.
          eapply (tids_proper) in Heq2.
          rewrite /op /cmra_op /dra_op //= /refine_op in Heq2.
          destruct le_dec; simpl in *; auto.
        }
        
        split.


        - eapply validity_car_proper in Heq1; auto. apply views_proper in Heq1.
        eapply validity_car_proper in Heq2; auto. apply views_proper in Heq2.
        rewrite -Hallsnap Heq1 Heq2.
        simpl.
        rewrite ?view_of_op. f_equal; auto.
        inversion Hcar_step; auto.

        - eapply validity_car_proper in Heq1; auto. apply cfgs_proper in Heq1.
        eapply validity_car_proper in Heq2; auto. apply cfgs_proper in Heq2.
        rewrite -fold_max_is_last_cfg; auto. rewrite ?Heq1 ?Heq2.
        simpl. rewrite Heqcs. rewrite ?app_assoc. rewrite last_snoc.
        rewrite Hunion_tids'. split_and!; auto.
         (csext ++ [c']). rewrite ?assoc. auto.
     Qed.

      Lemma allts_step_pres_ind (rs rs': list (iRes Λ (globalF Σ))) l n :
        Forall (λ rs, ✓{S n} (big_op rs)) (map fst l)
        ✓{S n} big_op rs'
        isteps_aux' (@idx_stepN (iResUR Λ (globalF Σ)) (S n)) l rs rs'
        view K (validity_car (big_op (map interp_extract rs))) = snapshot
        ( i : nat, i < fold_left Init.Nat.max
                                  (map (length fst) (cfgs K (validity_car
                                               (big_op (map interp_extract rs))))) 0
                                   i tids K (validity_car (big_op (map interp_extract rs))))
        view K (validity_car (big_op (map interp_extract rs'))) = snapshot
        ( i : nat, i < fold_left Init.Nat.max
                                  (map (length fst) (cfgs K (validity_car
                                               (big_op (map interp_extract rs'))))) 0
                                   i tids K (validity_car (big_op (map interp_extract rs'))))
       cfgs K (validity_car (big_op (map interp_extract rs))) `prefix_of`
             cfgs K (validity_car (big_op (map interp_extract rs'))).
      Proof.
        intros Hvalid ? Histeps Hforall. revert rs Hvalid Hforall Histeps. induction l; intros.
        - inversion Histeps; subst; auto.
        -
          inversion Histeps as [| ??? rs0 ? HR Haux]. subst. simpl in ×.
          inversion Haux as [| ??????]; subst.
          × eapply (allts_step_pres rs); eauto.
            apply Forall_inv in Hvalid; auto.
          × edestruct (IHl rs0) as (?&?&?); eauto.
            ** inversion Hvalid as [|??? Hvalid']; eauto.
            ** eapply (allts_step_pres rs); eauto.
               *** apply Forall_inv in Hvalid; auto.
               *** inversion Hvalid as [|??? Hvalid']. apply Forall_inv in Hvalid'; auto.
            ** eapply (allts_step_pres rs); eauto.
               *** apply Forall_inv in Hvalid; auto.
               *** inversion Hvalid as [|??? Hvalid']. apply Forall_inv in Hvalid'; auto.
            ** split_and!; auto. etransitivity; last eauto.
            edestruct (allts_step_pres rs rs0) as (?&?&?); eauto.
               *** apply Forall_inv in Hvalid; auto.
               *** inversion Hvalid as [|??? Hvalid']. apply Forall_inv in Hvalid'; auto.
      Qed.

        Lemma Forall4_Forall_extra_impl:
           (A B C D : Type) (P: A B C D Prop) Q R S T
            (U : D Prop)
            (l : list A) (k : list B) (k' : list C) (j : list D),
            Forall4 P l k k' j
            Forall Q l
            Forall R k
            Forall S k'
            Forall T j
            ( (x : A) (y : B) (z : C) (a : D), P x y z a Q x R y S z T a U a)
            Forall U j.
        Proof.
          induction 1; auto.
          do 4 inversion 1. subst.
          intros Himpl.
          econstructor. eapply Himpl; eauto. eapply IHForall4; eauto.
        Qed.
    Lemma ownle_interp_extract v tids cs ixs n r rl:
      ✓{n} rl
      ownle (refine v tids cs ixs) n r rl
      validity_car (interp_extract rl) Refine K v tids cs ixs.
    Proof.
      intros Hval.
      rewrite !ownle_eq /ownle_def ownGl_spec.
      rewrite /interp_extract /to_globalFe /refine.
      inversion 1 as [_ _ Hgst]. simpl in ×.
      specialize (Hgst (@inG_id Λ Σ _ (refine_inG))). rewrite iprod_lookup_singleton in Hgst.
      assert ((ucmra_transport (eq_sym inG_prf) (gst rl (@inG_id Λ Σ _ (refine_inG))))
                           ≡{n}≡
                           to_validity {| view := v; tids := tids; cfgs := cs; idxs := ixs |}).
      { rewrite -Hgst. rewrite ucmra_transport_sym_inv. auto. }
      inversion H0.
      rewrite H2. simpl. auto.
      eapply cmra_discrete_valid.
      eapply ucmra_transport_validN.
      destruct Hval as (_&_&Hgst_val).
      specialize (Hgst_val (@inG_id Λ Σ _ (refine_inG))). eapply cmra_validN_le; eauto. lia.
    Qed.
    Lemma isteps_aux'_hd_valid {A: ucmraT} (rs1 rs2: list A) l n:
        isteps_aux' (@idx_stepN A (S n)) l rs1 rs2
        ✓{S n} big_op rs2
        Forall (λ rs, ✓{S n} (big_op rs)) (map fst l)
        ✓{S n} (big_op rs1).
    Proof.
      induction 1; auto.
      intros Hval Hforall. apply Forall_inv in Hforall. auto.
    Qed.

    Lemma values_fixed_extension cfgs1 v ts σ csext ixs:
      valid_cfg_idx_seq (cfgs1 ++ [(of_val v :: ts, σ)] ++ csext) ixs
       ts' σ', last (cfgs1 ++ [(of_val v :: ts, σ)] ++ csext) =
                Some (of_val v :: ts', σ').
    Proof.
      induction csext as [|c'] using rev_ind.
      - simpl. rewrite last_snoc; eauto.
      - intros (is1a&is1b&?&?&?&Histeps)%valid_cfg_extract''.
        clear -Histeps.
        revert ts σ Histeps.
        induction is1b.
        × intros. inversion Histeps.
          subst. rewrite ?app_assoc last_snoc. eauto.
        × intros. inversion Histeps.
          subst. eapply idx_step_equiv in H1.
          inversion H1. subst. exfalso. eapply val_stuck in H6.
          rewrite to_of_val in H6. congruence.
          subst. edestruct IHis1b as (ts'&σ'&Hlast); eauto.
           ts', σ'. rewrite ?app_assoc ?last_snoc in Hlast ×.
          auto.
    Qed.

    Lemma last_ne_tl:
       {A} a (l: list A), last l = Some a l', l = l' ++ [a].
    Proof.
      intros ?? l Hlast. destruct l as [| a' l'] using rev_ind. simpl in *; congruence.
      rewrite last_snoc in Hlast. inversion Hlast. subst.
      eexists; eauto.
    Qed.

  Definition ht_adequacy_own_alt Λ Σ n Φ l e1 t2 σ1 m1 m2 σ2 :=
    @ht_adequacy_own Λ Σ Φ l e1 t2 σ1 m1 m2 σ2 n.

  Lemma ht_adequacy_refine (E: expr ) (e: expr Λ) v t2 (sσ: state ) (σ σ2: state Λ) Φ l:
  isteps idx_step l ([e], σ) (of_val v :: t2, σ2)
  Forall (λ e, ¬ reducible e σ2) (of_val v :: t2)
    {{ snapshot_ownl_exact {[0]} [([E], sσ)] []
                           ownP σ master_own_exact [([E], sσ)] [] }}
      e
      {{ λ v, ( V ES sσ', snapshot_ownl {[0]} ((of_val V :: ES), sσ')
                                          Φ v V) }}
     l' V T2 sσ2,
    isteps idx_step l' ([E], sσ) (of_val V :: T2, sσ2)
    ( i, ¬ (enabled idx_step (of_val V :: T2, sσ2)) i)
    Φ v V.
  Proof.
    intros Hsteps Hstopped Hht.
    rewrite /snapshot_ownl_exact /master_own_exact ?ownle_eq /ownle_def ?owne_eq /owne_def in Hht.
    assert (Forall (λ e, is_Some (to_val e)) (of_val v :: t2)) as Hvals.
    {
      eapply ht_adequacy_safe in Hsteps; eauto.
      - destruct Hsteps as [?|(t3&σ3&Hstep)]; auto.
         clear -Hstep Hstopped.
         inversion Hstep; subst.
         assert (e1 (of_val v :: t2)).
         { inversion H. rewrite H3. set_solver+. }
         rewrite Forall_forall in Hstopped ×. intros Hstopped.
         exfalso. eapply (Hstopped e1); eauto. inversion H; subst. do 3 eexists; eauto.
      - eapply master_snapshot_valid.
    }
    edestruct (@ht_adequacy_own_alt Λ (globalF Σ) (S (S (length l))))
      as (l'&rls2&rs2&Φs'&Hwptp&Hwsat&Histeps&Hsnd&Hinter_valid&Hestop);
      eauto using master_snapshot_valid.
    apply Forall4_cons_inv_l in Hwptp as
             (Φ'&Φs2&r&rs2'&rl&rls2'&HeqΦ&Heqrs&Heqrobs&Hwp1&Hwptp).
    inversion HeqΦ. subst.
    move: Hwp1. rewrite wp_eq. uPred.unseal⇒ /wp_value_inv Hwp1.
    rewrite pvs_eq in Hwp1.
    rewrite map_length in Hwsat.
    destruct (Hwp1 (S (S (length l'))) σ2 (big_op rs2') (big_op rls2') )
      as [r' (Hr'&?)]; rewrite ?right_id_L; auto.
    { rewrite map_length. split; omega. }
    { set_solver. }
    destruct Hr' as (V&ES&sσ'&(r1&r2&?rl1&rl2&Heqr&Heqrl&Hownl&(&Haff))).
    rewrite Haff ?right_id in Heqrl *=>Heqrl.
    rewrite -Heqrl /snapshot_ownl in Hownl ×. uPred.unseal.
    intros (cfg1&idxs1 &Hownl%ownle_interp_extract); simpl in *; auto.

     (idxs K (validity_car (interp_extract (big_op (rl :: rls2'))))).
     V.
    edestruct (operand_prefix_of_valid_seq (interp_extract rl) (interp_extract (big_op rls2')))
     as (Hcfgs_prefix&Hisext_prefix).
    {
      rewrite -interp_extract_op.
      eapply (interp_extract_validN' _ (S (length l'))); eauto.
      eapply wsat_valid in H.
      eapply cmra_validN_op_r. eapply H.
      lia.
    }
               

    edestruct Hcfgs_prefix as (csext&Heq_csext).
    generalize (cfgs_proper _ _ _ _ Hownl); intros Hrl_cfgs.
    generalize (tids_proper _ _ _ _ Hownl); intros Hrl_tids.
rewrite Hrl_cfgs in Heq_csext.
    simpl in ×.
    rewrite -app_assoc in Heq_csext.
    assert ( (interp_extract (rl big_op rls2'))) as Hval.
    {
      apply (interp_extract_validN' _ (S (length l'))).
      eapply wsat_valid in H.
      eapply cmra_validN_op_r. eapply H.
      lia.
    }
    assert ( (validity_car (interp_extract (rl big_op rls2')))) as Hval_car.
    {
      eapply validity_valid_car_valid. eauto.
    }
    destruct Hval_car as (_&Hval_cfgs).
    erewrite (validity_car_proper (interp_extract (rl big_op rls2'))) in Hval_cfgs;
      simpl in *; eauto using interp_extract_op.
    rewrite validity_car_op in Hval_cfgs. rewrite Heq_csext in Hval_cfgs.
    edestruct values_fixed_extension as (T2&sσ2&Histeps'); eauto.
    { apply Hval_cfgs. }
     T2, sσ2.
    edestruct allts_step_pres_ind as (Hallsnap&Hallts&Hcfgs_ext); simpl; eauto.
    { rewrite map_length. eauto.
      eapply wsat_valid in Hwsat. simpl.
      eapply cmra_validN_op_r. eapply Hwsat.
      lia.
    }
    {simpl. rewrite /interp_extract /to_globalFe //=.
      rewrite ?iprod_lookup_singleton ucmra_transport_sym_inv. simpl. auto. }
    { intros i.
      simpl. rewrite /interp_extract /to_globalFe //=.
      rewrite ?iprod_lookup_singleton ucmra_transport_sym_inv. simpl.
      set_unfold. omega. }
    split_and!.
    - move: Hcfgs_ext.
      simpl. rewrite {1}/interp_extract {1}/to_globalFe //=.
      rewrite ?iprod_lookup_singleton ucmra_transport_sym_inv. simpl.
      intros Hcfgs_ext.
      destruct Hcfgs_ext as (csinit&Heq_csinit).
      assert (hd_error (cfg1 ++ (of_val V :: ES, sσ') :: csext) = Some ([E], sσ)).
      {
        erewrite <-(validity_car_proper (interp_extract (big_op rls2'))
                                        (big_op (map interp_extract rls2'))) in Heq_csinit;
          simpl in *; last (eapply interp_extract_bigop).
        × rewrite Heq_csext in Heq_csinit.
          rewrite Heq_csinit. auto.
        × eapply (interp_extract_validN' _ (S (length l'))); eauto.
          apply wsat_valid in Hwsat.
          first [ solve_validN || solve_validN' ]; omega.
          omega.
          }
      simpl in ×.
      eapply valid_cfg_extract''''; eauto.
    erewrite (validity_car_proper (interp_extract (rl big_op rls2')));
      simpl in *; eauto using interp_extract_op.
    eauto.
    - intros i Henabledi.
        assert (i tids K (validity_car (interp_extract rl)
                                            validity_car (interp_extract (big_op rls2')))).
        {
          specialize (Hallts i).
          erewrite (validity_car_proper (interp_extract (big_op rls2'))
                                          (big_op (map interp_extract rls2')));
          last (eapply interp_extract_bigop).
          eapply Hallts.
          rewrite -fold_max_is_last_cfg; auto.
          simpl.
          rewrite (validity_car_proper (interp_extract (big_op rls2'))
                                          (big_op (map interp_extract rls2'))) in Heq_csext *;
          simpl in *; last (eapply interp_extract_bigop).
          intros →. rewrite Histeps'.
          simpl.
          destruct Henabledi as (?&Hidx_step).
          eapply length_cfg_idx_step2 in Hidx_step. simpl in ×. auto.
         eapply (interp_extract_validN' _ (S (length l'))); eauto.
         { eapply wsat_valid in Hwsat. solve_validN; omega. omega. }
         eapply (interp_extract_big_op_validN' _ (S (length l'))); eauto.
         { eapply wsat_valid in Hwsat. solve_validN; omega. omega. }
         eapply (interp_extract_validN' _ (S (length l'))); eauto.
         { eapply wsat_valid in Hwsat. solve_validN; omega. omega. }
        }
      assert (tids K (validity_car (big_op (map interp_extract (rl :: rls2'))))
              = tids K
                     (validity_car (interp_extract rl)
                                    validity_car (interp_extract (big_op rls2')))) as Heq_tids.
        {
          eapply tids_proper.
          simpl map. rewrite big_op_cons.
          rewrite (validity_car_proper (interp_extract (big_op rls2'))
                                          (big_op (map interp_extract rls2'))); auto.
          eapply (interp_extract_validN' _ (S (length l'))); eauto.
         { eapply wsat_valid in Hwsat. solve_validN; omega. omega. }
          eapply interp_extract_bigop.
        }
        edestruct (big_op_tids_split (map interp_extract (rl :: rls2')))
          as (rls'_left&rls'_right&rli&n&Heq_rs&Hlen&Hin_r).
        { rewrite Heq_tids. eauto. }
        simpl in Heq_rs.

    assert (Forall (λ r', rs', r' big_op rs' r big_op rs2') rs2').
    {
      eapply Forall_forall.
      intros x Hin.
      edestruct (elem_of_list_split rs2') as (s1&s2&Heq); eauto.
      rewrite Heq. (r :: (s1 ++ s2)).
      simpl. rewrite ?big_op_app. simpl.
      solve_equiv.
    }
    assert (Forall (λ r', rls'_left rls'_right,
                       rl :: rls2' = rls'_left ++ r' :: rls'_right) rls2').
    {
      eapply Forall_forall.
      intros x Hin.
      edestruct (elem_of_list_split rls2') as (s1&s2&Heq); eauto.
       (rl :: s1), s2. rewrite Heq. eauto.
    }


        assert ( x, snap_vector x = map (interp_extract) (rl :: rls2')) as (x&Hsvx_eq).
        {
          refine (ex_intro _ {| snap_vector := map interp_extract (rl :: rls2') ;
                           compatible := _;
                           all_snaps := _;
                           all_ne := _;
                           all_threads := _|} _); auto.
          Unshelve.
          - eapply (interp_extract_big_op_validN' _ (S (S (length l')))). simpl in *; eauto.
            { eapply wsat_valid in Hwsat. solve_validN; omega. omega. }
          - eapply bigop_snap_iff. auto.
          - simpl.
          rewrite <-(validity_car_proper (interp_extract (big_op rls2'))
                                          (big_op (map interp_extract rls2'))); auto.
          rewrite Heq_csext. destruct cfg1; simpl in *; congruence.
          eapply (interp_extract_validN' _ (S (length l'))); eauto.
            { eapply wsat_valid in Hwsat. solve_validN; omega. omega. }
          eapply interp_extract_bigop.
          - eauto.
        }
        assert ( cs, cfgs K (validity_car (big_op (snap_vector x)))
                      = cs ++ [(of_val V :: T2, sσ2)]) as (cs00&Heq_cs00).
        {
          rewrite Hsvx_eq.
          simpl in ×.

          eapply last_ne_tl in Histeps' as (cs'&Heq).
           cs'.
          rewrite <-(validity_car_proper (interp_extract (big_op rls2'))
                                          (big_op (map interp_extract rls2'))); auto.
          rewrite Heq_csext Heq. auto.
          eapply (interp_extract_validN' _ (S (length l'))); eauto.
            { eapply wsat_valid in Hwsat. solve_validN; omega. omega. }
          eapply interp_extract_bigop.
        }
        
        assert (Forall (λ rl,
                         i, i tids K (validity_car (interp_extract rl))
                          ¬ enabled idx_step (of_val V :: T2, sσ2) i) rls2') as Hrest_stuck.
        {
          eapply Forall4_Forall_extra_impl; eauto.
          { inversion Hvals; eauto. }
          clear -Hwsat Heq_csext K_nz PrimDet PrimDec Heq_cs00 Hsvx_eq.
          intros e Φ r' rl' Hwp Hval Hstopped Hcompose Hcomposel.
          destruct Hcomposel as (rls'_left&rls'_right&Hequiv_rls).
          assert ( r, uPred_holds (uPred_stopped) (S (S (length l'))) r rl')
            as (r'' & Hstopped_rl').
          {
          simpl in ×.
          destruct Hval as (v&Heq).
          edestruct (of_to_val e v); eauto.
          move: Hwp. rewrite wp_eq. uPred.unseal⇒ /wp_value_inv Hwp.
          rewrite pvs_eq in Hwp.
          destruct Hcompose as (rs'&Hequiv_rs).
          destruct (Hwp (S (S (length l'))) σ2 (big_op rs') (big_op rls'_left big_op rls'_right) ) as (r''&&Hwsat').
          { rewrite map_length. split; omega. }
          { set_solver. }
          { rewrite Hequiv_rs. apply (f_equal big_op) in Hequiv_rls.
            simpl in Hequiv_rls.
            rewrite assoc. rewrite (comm _ rl').
            rewrite -assoc.
            rewrite -(big_op_cons rl').
            rewrite -(big_op_app). rewrite -Hequiv_rls right_id_L. auto. }
           r''.
          move: (Hstopped v). uPred.unsealHstopped'. eapply Hstopped'; eauto.
            { eapply wsat_valid in Hwsat'. solve_validN; omega. omega. }
            { eapply wsat_valid in Hwsat'. solve_validN; omega. omega. }
          }
          intros i Hin Henabled.
          move: Hstopped_rl'. uPred.unseal. rewrite /uPred_holds //=.
          intros Hnf. specialize (Hnf 1).
          edestruct Hnf; first omega.
          edestruct (step_block_or_none_enabled (of_val V :: T2, sσ2)
                                                (tids K (validity_car (interp_extract rl'))))
                    as [Hstep_block|Hnone_enabled].
         - edestruct (step_block_interp_codomain x) as (x'&Hstep_xn); eauto.
          { rewrite Hsvx_eq.
            apply (f_equal (map interp_extract)) in Hequiv_rls.
            rewrite Hequiv_rls. simpl. rewrite map_app //=. }
         rewrite /interp_step' in Hstep_xn.
         edestruct idx_step_inv_big as (r1&r2&rs&Hstep&_&_&_&rls_left'&rls_right'&Hsvx_eq'&Hlen);
            eauto.
         rewrite Hsvx_eq in Hsvx_eq'. rewrite Hequiv_rls in Hsvx_eq'.
         rewrite map_app in Hsvx_eq'. simpl in ×. apply app_inj_1 in Hsvx_eq' as (Heq1&Heq2).
         inversion Heq2; subst.
         edestruct interp_extract_step_reflect as (y&Hstep_y&Hinterp); eauto.
         rewrite Hlen. auto.
         - exfalso; eapply (Hnone_enabled i); eauto.
        }
        destruct rls'_left.
        + simpl in ×. inversion Heq_rs. subst.
          rewrite Hrl_tids in Hin_r. assert (i = 0) by (clear -Hin_r; set_solver).
          subst.
          inversion Henabledi as [? Hstep]. apply idx_step_equiv in Hstep.
          inversion Hstep as [? ? ? ? ? ? Hprim|]. subst. eapply val_stuck in Hprim.
          rewrite to_of_val in Hprim. congruence.
        + simpl in ×. inversion Heq_rs as [(Hhd&Heq_rs')].
          edestruct (elem_of_map_inv interp_extract rls2' rli) as (rl0&Hin&Hinterp).
          { rewrite Heq_rs'. set_solver+. }
          rewrite Forall_forall in Hrest_stuck *=>Hrest_stuck.
          specialize (Hrest_stuck rl0).
          eapply Hrest_stuck; eauto. rewrite Hinterp. auto.
    - clear -. move: . rewrite /uPred_holds //=.
    - eapply wsat_valid in Hwsat. solve_validN; omega. omega.
      Qed.

  Lemma ht_adequacy_inf_refine (E: expr ) (e: expr Λ) (sσ: state ) (σ: state Λ)
        (tr: trace idx_step ([e], σ)) Φ:
    {{ snapshot_ownl_exact {[0]} [([E], sσ)] []
                           ownP σ master_own_exact [([E], sσ)] [] }}
      e
      {{ λ v, ( V ES sσ', snapshot_ownl {[0]} ((of_val V :: ES), sσ')
                                          Φ v V) }}
     (tr': trace idx_step ([E], sσ)),
      fair_pres _ _ tr tr'.
  Proof.
    intros Hht.
    edestruct (@ht_adequacy_own_inf_hom2_alt Λ (globalF Σ) (interp_cod_cofeT) interp_step interp
                                             (λ v, ( V ES sσ', snapshot_ownl {[0]} (of_val V :: ES, sσ') Φ v V))%I
                                             e σ tr
                                             (to_globalFe (refine snapshot {[0]} [([E], sσ)] []))
                                             (to_globalFe (refine master [([E], sσ)] []))
                                             3); eauto.
    - intros n x y Heq.
      unfold interp.
      assert (( big_op (map interp_extract x))
                                                ( big_op (map interp_extract y))) as Hiff_val.
      {
        split.
        - intros; rewrite -Heq; auto.
        - intros; rewrite Heq; auto.
      }
      
      
      eapply sumbool_iff_case; auto.
      intros prf1x prf1y.

      assert
        (( r : validity _,
             r map interp_extract x view K (validity_car r) = snapshot)
                                                                               ( r : validity _,
                                                                                   r map interp_extract y view K (validity_car r) = snapshot)) as Hiff_snap.
      {
        split.
        - intros Hsnapx r Hin.
          eapply (elem_of_equiv_list _ _ (map interp_extract x)) in Hin as (r'&?&Hequiv).
          transitivity (view K (validity_car r')); last eapply Hsnapx.
          eapply views_proper. symmetry. eapply validity_car_proper.
          × eapply elem_of_big_op_valid; first eapply prf1x. eauto.
          × symmetry; auto.
          × auto.
          × eapply map_proper. eapply interp_extract_proper. auto.
        - intros Hsnapx r Hin.
          eapply (elem_of_equiv_list _ _ (map interp_extract y)) in Hin as (r'&?&Hequiv).
          transitivity (view K (validity_car r')); last eapply Hsnapx.
          eapply views_proper. symmetry. eapply validity_car_proper.
          × eapply elem_of_big_op_valid; first eapply prf1y. eauto.
          × symmetry; auto.
          × auto.
          × eapply map_proper. eapply interp_extract_proper. auto.
      }
      
      
      eapply sumbool_iff_case; auto.
      intros prf2x prf2y.

      assert (validity_car (big_op (map interp_extract x)) =
              validity_car (big_op (map interp_extract y))) as Heqvc.
      {
        rewrite -leibniz_equiv_iff.
        apply validity_car_proper; auto.
        rewrite Heq; auto.
      }
      assert (cfgs K (validity_car (big_op (map interp_extract x))) =
              cfgs K (validity_car (big_op (map interp_extract y)))) as Heqcfgs.
      { rewrite Heqvc. auto. }
      
      eapply sumbool_iff_case; auto.
      { rewrite Heqcfgs. auto. }
      
      intros prf3x prf3y.
      assert
        ( x y, x y (big_op (map interp_extract x))
                ( i : nat,
                    i <
                    fold_left Init.Nat.max
                              (map (length fst)
                                   (cfgs K (validity_car (big_op (map interp_extract x))))) 0
                               i tids K (validity_car (big_op (map interp_extract x))))
                (( i : nat,
                     i <
                     fold_left Init.Nat.max
                               (map (length fst)
                                    (cfgs K (validity_car (big_op (map interp_extract y))))) 0
                                i tids K (validity_car (big_op (map interp_extract y)))))) as Hmax.
      {
        clear.
        intros x y Hequiv Hval.
        intros Hlt i.
        assert (validity_car (big_op (map interp_extract x)) =
                validity_car (big_op (map interp_extract y))) as Heq_vc.
        { rewrite -leibniz_equiv_iff. apply validity_car_proper; auto.
          rewrite Hequiv. auto. }
        split; intros Hin.
        - erewrite tids_proper; first eapply Hlt; auto.
          erewrite (cfgs_proper _ _ _ Heq_vc).
          eapply Hin.
        - erewrite <-(cfgs_proper _ _ _ Heq_vc).
          eapply Hlt. erewrite tids_proper; first eauto; auto.
      }
      
      eapply sumbool_iff_case; auto.
      { split; eapply Hmax; eauto. }
      intros prf4x prf4y.
      econstructor. rewrite /equiv /cofe_equiv //= /interp_equiv.
      simpl. rewrite Heq. auto.
    - intros n mx my Hequiv mx' my' Hequiv'.
      unfold interp_step.
      destruct Hequiv as [x y Hequiv|]; auto.
      destruct Hequiv' as [x' y' Hequiv'|]; auto.
      rewrite Hequiv Hequiv'. auto.
    - intros n i robs robs' Hval Hval' Histep Hinterp_good.
      eapply interp_not_none_inv in Hinterp_good as (x&Heq).
      assert (snap_vector x = map interp_extract robs) as Hsvx_ie by (eapply interp_some_inv; eauto).
      destruct x as [svx compat allsnap ne allts]. simpl in ×.
      cut (interp (S n) robs' None).
      {
        intros Hinterp_good'. split; auto.
        eapply interp_not_none_inv in Hinterp_good' as (x'&Heq').
        rewrite Heq Heq'. simpl.
        rewrite Hsvx_ie.
        erewrite (interp_some_inv _ robs'); eauto.
        eapply idx_stepN_map_extract; eapply idx_stepN_le; last apply Histep.
        omega.
      }
      

 
      eapply idx_stepN_map_extract in Histep.
      eapply idx_step_inv_big in Histep as (r1&r2&rs&Hstep&Heq1&Heq2&Hlen).
      inversion Hstep as [Hcov Hcar_step].
      assert ( r1 r2 validity_car r1 validity_car (big_op rs) validity_car r2
               validity_car r1 validity_car (big_op rs)) as
          (Hvalr1&Hvalr2&Hvalcr1&Hvalcrs&Hvalcr2&Hdisj).
      {
        apply interp_extract_validN in Hval.
        rewrite interp_extract_bigop in Hval ×.
        rewrite Heq1. inversion 1 as (?&?&?); auto.
        split_and!.
        - auto.
        - eapply Hcov; eauto.
        - destruct r1; eauto.
        - destruct (big_op rs); eauto.
        - assert ( r2). apply Hcov. eauto. destruct r2; auto.
        - auto.
      }
      assert (tids K (validity_car (big_op svx))
              = tids K (validity_car r1) tids K (validity_car (big_op rs)))
        as Hunion_tids.
      {
        rewrite -Hsvx_ie in Heq1.
        eapply validity_car_proper in Heq1; eauto.
        simpl in Heq1.
        eapply (tids_proper) in Heq1.
        rewrite /op /cmra_op /dra_op //= /refine_op in Heq1.
        destruct le_dec; simpl in *; auto.
      }
      specialize (Hcar_step Hvalr1).
      edestruct (refine_step_disjoint_all_threads' K (validity_car r1)
                                                   (validity_car (big_op rs))
                                                   (validity_car r2))
        as (_&_&c'&csext&isext&_&Heqcs&_&_&_&Hall&_); eauto.
      {
        apply interp_extract_validN in Hval'.
        rewrite interp_extract_bigop in Hval' ×.
        rewrite Heq2. inversion 1 as (?&?&?); auto.
      }
      {
        generalize allts.
        rewrite -fold_max_is_last_cfg.
        intros allts'. intros i'.
        rewrite Hunion_tids in allts'.
        rewrite -(allts' i').
        rewrite Hsvx_ie. apply validity_car_proper in Heq1; auto.
        rewrite Heq1. simpl. auto.
        generalize compat. rewrite Hsvx_ie. auto.
        auto.
      }
      
      
      assert ( big_op (map interp_extract robs')).
      {
        rewrite -interp_extract_bigop. eapply interp_extract_validN; auto.
        eauto.
      }
      
      eapply interp_some.
      × rewrite -interp_extract_bigop. eapply interp_extract_validN; auto.
      ×
        
        
        idtac. eapply bigop_snap_iff.
        eapply validity_car_proper in Heq2; auto.
        rewrite Heq2.
        simpl. apply op_snap_iff. split.
        ** inversion Hcar_step; auto.
        ** generalize allsnap. rewrite bigop_snap_iff.
           eapply validity_car_proper in Heq1. rewrite Hsvx_ie. rewrite Heq1.
           simpl. intros (?&?)%op_snap_iff. auto.
           rewrite -Hsvx_ie; auto.
      × eapply validity_car_proper in Heq2; auto.
        rewrite Heq2. simpl. rewrite Heqcs.
        intro Hfalse. symmetry in Hfalse.
        eapply app_cons_not_nil. rewrite ?app_assoc in Hfalse. eauto.
      ×
        
        assert (tids K (validity_car (big_op (map interp_extract robs')))
                = tids K (validity_car r2) tids K (validity_car (big_op rs)))
          as Hunion_tids'.
        {
          eapply validity_car_proper in Heq2; eauto.
          simpl in Heq2.
          eapply (tids_proper) in Heq2.
          rewrite /op /cmra_op /dra_op //= /refine_op in Heq2.
          destruct le_dec; simpl in *; auto.
        }
        
        eapply validity_car_proper in Heq2; auto. apply cfgs_proper in Heq2.
        rewrite -fold_max_is_last_cfg; auto. rewrite Heq2.
        simpl. rewrite Heqcs. rewrite ?app_assoc. rewrite last_snoc.
        rewrite Hunion_tids'. auto.
    - intros n i robs Henabled.
      destruct Henabled as (my&Hstep).
      specialize (interp_some_inv (S n) robs).
      intros Hsome.
      destruct (interp (S n) robs) as [x|];
        destruct my as [y|]; try (inversion Hstep; done).

      inversion Hstep as [r1 r2 t1 t2 t1' t2' Heq1 Heq2 Hstep' Hlen Hequiv Hequiv'|
                          r1 r2 rf t1 t2 t1' t2' Heq1 Heq2 Hstep' Hlen Hequiv Hequiv'].
      × rewrite (Hsome x) in Heq1; auto.
        assert (r1 _(S n) r2) as Hstep'_Sn.
        { inversion Hstep'. econstructor; eauto. }
        apply map_app_inv in Heq1 as (t1_0&?&Heq_robs&Heq_t1&Heq_right).
        apply map_cons_inv in Heq_right as (r1_0&t2_0&->&Heq_r1&Heq_t2).
        rewrite -Heq_r1 in Hstep'_Sn.
        edestruct interp_extract_step_reflect as (r2_0&Hstep''&Heq_r2); eauto.
         (t1_0 ++ r2_0 :: t2_0).
        econstructor; eauto.
        rewrite <-(map_length interp_extract); rewrite Heq_t1. auto.
      × rewrite (Hsome x) in Heq1; auto.
        assert (r1 _(S n) r2 rf) as Hstep'_Sn.
        { inversion Hstep'. econstructor; eauto. }
        apply map_app_inv in Heq1 as (t1_0&?&Heq_robs&Heq_t1&Heq_right).
        apply map_cons_inv in Heq_right as (r1_0&t2_0&->&Heq_r1&Heq_t2).
        rewrite -Heq_r1 in Hstep'_Sn.
        edestruct interp_extract_step_reflect as (r2_0&Hstep''&Heq_r2); eauto.
         (t1_0 ++ r2_0 :: t2_0).
        econstructor; eauto.
        rewrite <-(map_length interp_extract); rewrite Heq_t1. auto.
    - eapply interp_step_bounded_nondet.
    - eapply interp_some.
      × simpl. unfold interp_extract. simpl.
        unfold to_globalFe. rewrite iprod_lookup_singleton.
        rewrite ucmra_transport_sym_inv. rewrite right_id.
        constructor.
        ** simpl. set_unfold. intros n; omega.
        ** simpl. econstructor.
      × simpl. unfold interp_extract. simpl.
        unfold to_globalFe. rewrite iprod_lookup_singleton.
        rewrite ucmra_transport_sym_inv. set_unfold.
        intros r [->|Hf]; last exfalso; auto.
      × simpl. unfold interp_extract. simpl.
        unfold to_globalFe. rewrite iprod_lookup_singleton.
        rewrite ucmra_transport_sym_inv. set_unfold.
        auto.
      × simpl. unfold interp_extract. simpl.
        unfold to_globalFe. rewrite iprod_lookup_singleton.
        rewrite ucmra_transport_sym_inv. do 2 set_unfold.
        intros x; omega.
    - unfold to_globalFe.
      intros i. case (decide (i = (@inG_id Λ Σ _ (refine_inG)))).
      × intros →. rewrite iprod_lookup_op.
        rewrite ?iprod_lookup_singleton.
        rewrite -ucmra_transport_op.
        rewrite ucmra_transport_valid. split_and!.
        ** econstructor.
           *** simpl. set_unfold. intros; omega.
           *** simpl. econstructor.
        ** econstructor.
           *** simpl. set_unfold. intros; omega.
           *** simpl. econstructor.
        ** simpl.
           replace (@nil nat) with (@nil nat ++ @nil nat) at 2; last auto.
           replace ([([E], sσ)]) with ([([E], sσ)] ++ []) at 2; last auto.
           econstructor.
           *** set_solver.
           *** set_solver.
      × intros Hne. rewrite iprod_lookup_op. rewrite ?iprod_lookup_singleton_ne; auto.
        rewrite right_id. eapply ucmra_unit_valid.
    - rewrite /snapshot_ownl_exact ownle_eq /ownle_def
              /master_own_exact owne_eq /owne_def in Hht.
      eauto.
    - econstructor; simpl; auto.

        idtac. intros.
        apply uPred.exist_elimV.
        apply uPred.exist_elimEs.
        apply uPred.exist_elimsσ'.
        eapply (own_value_stopped (Φ v V)); eauto.

    -
      
      
      
      assert ( x', (interp 3
                            [Res (to_globalFe (refine snapshot {[0]} [([E], sσ)] []))]) = Some x') as (x'&Hx').
      {
        inversion x. destruct (interp 3); first eexists; eauto.
        inversion H0.
      }
      assert (fst (interp_flatten x') = ([E], sσ)) as Heq_ifx'.
      {
        unfold interp_flatten.
        eapply interp_some_inv in Hx'.
        destruct x'. simpl in ×.
        clear -Hx' compatible0.
        assert (cfgs K (validity_car (big_op
                                           [interp_extract
                                              (Res (to_globalFe (refine snapshot {[0]} [([E], sσ)] [])))])) = [([E], sσ)]).
        {
          simpl big_op. erewrite validity_car_proper; last (rewrite right_id; auto).
          unfold interp_extract. simpl. unfold to_globalFe.
          rewrite iprod_lookup_singleton.
          rewrite ucmra_transport_sym_inv. simpl. auto.
          unfold interp_extract. simpl. unfold to_globalFe.
          rewrite iprod_lookup_singleton. rewrite ucmra_transport_sym_inv.
          rewrite Hx' in compatible0. simpl in compatible0.
          unfold interp_extract, to_globalFe in compatible0. simpl in ×.
          rewrite iprod_lookup_singleton in compatible0.
          rewrite ucmra_transport_sym_inv in compatible0.
          auto.
        }
        
        rewrite Hx' in all_ne0 ×.
        rewrite H in all_ne0 ×.
        simpl. auto.
      }
      
      rewrite Hx' in x H.
      edestruct (some_interp_extract x' x); eauto.
      edestruct (flatten_fair_pres_alt interp_flatten x0 (idx_step)) as (trf&?).
      × intros i a a' Histep.
        eapply idx_step_inv_big in Histep as (r1&r2&rs&Hstep&Heq1&Heq2&Hlen&(t1&t2&Heq&Hlen_t1)).
        inversion Hstep as [Hcov Hcar_step].
        destruct a as [sva Hcompat all_snap all_ne all_ts].
        destruct a' as [sva' Hcompat' all_snap' all_ne' all_ts'].
        assert ( r1 r2 validity_car r1 validity_car (big_op rs) validity_car r2
                 validity_car r1 validity_car (big_op rs)) as
            (Hvalr1&Hvalr2&Hvalcr1&Hvalcrs&Hvalcr2&Hdisj).
        {
          simpl in ×. rewrite Heq1 in Hcompat ×.
          inversion 1 as (?&?&?); auto.
          split_and!.
          - auto.
          - eapply Hcov; eauto.
          - destruct r1; eauto.
          - destruct (big_op rs); eauto.
          - assert ( r2). apply Hcov. eauto. destruct r2; auto.
          - auto.
        }
        assert (tids K (validity_car (big_op sva))
                = tids K (validity_car r1) tids K (validity_car (big_op rs)))
          as Hunion_tids.
        {
          eapply validity_car_proper in Heq1; eauto.
          simpl in Heq1.
          eapply (tids_proper) in Heq1.
          rewrite /op /cmra_op /dra_op //= /refine_op in Heq1.
          destruct le_dec; simpl in *; auto.
        }
        specialize (Hcar_step Hvalr1).
        edestruct (refine_step_disjoint_all_threads' K (validity_car r1)
                                                     (validity_car (big_op rs))
                                                     (validity_car r2))
          as (cs0&c0&c'&csext&isext&Heqcs0&Heqcs&?&?&?&Hall&Hstep_enabled&Histeps); eauto.
        {
          simpl in ×. rewrite Heq2 in Hcompat' ×.
          inversion 1 as (?&?&?); auto.
        }
        {
          generalize all_ts.
          rewrite -fold_max_is_last_cfg.
          intros allts'. intros i'.
          rewrite Hunion_tids in allts'.
          rewrite -(allts' i').
          apply validity_car_proper in Heq1; auto.
          rewrite Heq1. simpl. auto.
          auto.
        }
        rewrite (interp_flatten_last _ cs0 c0); last first.
        {
          simpl. rewrite -Heqcs0.
          eapply cfgs_proper.
          rewrite validity_car_proper; eauto.
          simpl. auto.
        }
        rewrite (interp_flatten_last _ (cs0 ++ [c0] ++ csext) c'); last first.
        {
          simpl. eapply validity_car_proper in Heq2; simpl; auto.
          rewrite Heq2. simpl. rewrite Heqcs. rewrite Heqcs0. rewrite -?app_assoc. simpl.
          auto.
        }
        rewrite (interp_flatten_nth_map_tids _ t1 t2 r1 i).
         isext; auto.
        simpl; auto.
        simpl; auto.
      × intros a i Henabled.
        destruct a as [sva Hcompat Hsnaps Hne Hallts].
        assert ( cs c, cfgs K (validity_car (big_op sva)) = cs ++ [c]) as (cs&c&Heqcs).
        {
          clear -Hne.
          destruct cfgs as [| c cs] using rev_ind; first congruence.
           cs, c. auto.
        }
        rewrite (interp_flatten_last _ cs c) in Henabled; auto.
        assert (i tids K (validity_car (big_op sva))).
        {
          eapply Hallts. rewrite -fold_max_is_last_cfg; auto.
          rewrite Heqcs. rewrite last_snoc; simpl.
          destruct Henabled.
          eapply length_cfg_idx_step2.
          eauto.
        }
        edestruct big_op_tids_split as (t1&t2&r&n&Heq&Hlen&Hin); eauto.
         n. rewrite (interp_flatten_nth_map_tids _ t1 t2 r n); auto.
      × intros a i j (Henabled&Hin).
        edestruct (interp_flatten_to_natset a j) as (ns&Hns_spec).
        edestruct (step_block_or_none_enabled (fst (interp_flatten a)) ns)
          as [Hblock|Hnone_enabled].
        ** edestruct interp_flatten_in_split_sv as (t1&t2&r&Hsva_eq&Hlen&Hset); eauto.
           edestruct (interp_flatten_last_inv a) as (cs&Hsva_cs_eq).
           edestruct (step_block_interp_codomain); eauto.
           rewrite -leibniz_equiv_iff. set_unfold.
           intros k. rewrite Hns_spec. rewrite Hset. set_solver+.
           eexists; eauto.
        ** exfalso. eapply (Hnone_enabled i); auto.
           eapply Hns_spec; eauto.
      × intros a i Henabled.
        destruct Henabled as (b&His).
        unfold interp_step' in His.
        eapply idx_step_inv_big in His as (r1&r2&rs&Histep&Heq1&Heq2&?&t1&t2&Heqa&Hlen).
        erewrite interp_flatten_nth_map_tids; eauto.
        assert ( r1 r2 validity_car r1 validity_car (big_op rs) validity_car r2
                 validity_car r1 validity_car (big_op rs)
                 validity_car (r1 big_op rs)
                 validity_car (r2 big_op rs)) as
            (Hvalr1&Hvalr2&Hvalcr1&Hvalcrs&Hvalcr2&Hdisj&Hvalprod1&Hvalprod2).
        {
          simpl in ×. destruct a as [sva Hcompat ? ? ?]. simpl in ×. rewrite Heq1 in Hcompat ×.
          inversion 1 as (?&?&?); auto.
          split_and!.
          - auto.
          - inversion Histep as [Hcov ?]. eapply Hcov; eauto.
          - destruct r1; eauto.
          - destruct (big_op rs); eauto.
          - assert ( r2). inversion Histep as [Hcov ?]. apply Hcov. eauto. destruct r2; auto.
          - auto.
          - eapply dra_op_valid; try apply validity_prf; eauto.
          - simpl in ×. destruct b as [svb Hcompat' ? ? ?]. simpl in ×. rewrite Heq2 in Hcompat' ×.
            inversion 1 as (?&?&?). eapply dra_op_valid; try apply validity_prf; eauto.
        }
        inversion Histep as [Hcov Histep'].
        specialize (Histep' Hvalr1).
        destruct a as [sva ? ? ? all_ts].
        assert (tids K (validity_car (big_op sva))
                = tids K (validity_car r1) tids K (validity_car (big_op rs)))
          as Hunion_tids.
        {
          eapply validity_car_proper in Heq1; eauto.
          simpl in Heq1.
          eapply (tids_proper) in Heq1.
          rewrite /op /cmra_op /dra_op //= /refine_op in Heq1.
          destruct le_dec; simpl in *; auto.
        }
        edestruct (refine_step_disjoint_all_threads' K (validity_car r1) (validity_car (big_op rs)))
          as (cs0&c0&c'&csext&isext&Heqcs0&Heqcs&Heqis&?&?&Hall&Hstep_enabled&Histeps); eauto.
        {
          simpl in ×. destruct b as [svb Hcompat' ? ? ?]. simpl in ×. rewrite Heq2 in Hcompat' ×.
          inversion 1 as (?&?&?); auto.
        }
        {
          generalize all_ts.
          rewrite -fold_max_is_last_cfg.
          intros allts'. intros i'.
          rewrite Hunion_tids in allts'.
          rewrite -(allts' i').
          apply validity_car_proper in Heq1; auto.
          rewrite Heq1. simpl. auto.
          auto.
        }
        
        rewrite (interp_flatten_last _ cs0 c0); last first.
        {
          simpl. rewrite -Heqcs0.
          eapply cfgs_proper.
          rewrite validity_car_proper; eauto.
          simpl. auto.
        }
        destruct Hvalprod1 as [? Hval_cfg1].
        destruct Hvalprod2 as [? Hval_cfg2].
        simpl in Hval_cfg1, Hval_cfg2.
        rewrite Heqcs0 in Hval_cfg1.
        rewrite Heqcs Heqcs0 Heqis in Hval_cfg2.
        rewrite -assoc in Hval_cfg2.
        eapply valid_seq_split in Hval_cfg2; last first.
        { eapply valid_cfg_idx_length4; eauto. }
        destruct isext as [| i' isext'].
        ** exfalso. inversion Hval_cfg2. destruct csext; simpl in *; congruence.
        ** i'. split.
           *** clear PrimDet PrimDec. set_solver.
           *** inversion Hval_cfg2; subst. eexists; eauto.
      × intros a b n.



        inversion 1 as [r1 r2 t1 t2 t1' t2' Heqa Heqb ? Hlen Hequiv1 Hequiv2|
                        r1 r2 rf t1 t2 t1' t2' Heqa Heqb ? Hlen Hequiv1 Hequiv2]; subst.
        ** intros j Hlen.
           assert (length t1 = length t1') as Hlen1.
           { rewrite Hequiv1; auto. }
           assert (length t2 = length t2') as Hlen2.
           { rewrite Hequiv2; auto. }
           
           assert ( big_op t1) as Hvalt1.
           { destruct a as [sva Hcompata ? ? ?].
             simpl in ×. clear -Heqa Hcompata. rewrite Heqa in Hcompata.
             rewrite big_op_app in Hcompata *; auto.
           }
           assert ( big_op t2) as Hvalt2.
           { destruct a as [sva Hcompata ? ? ?].
             simpl in ×. clear -Heqa Hcompata. rewrite Heqa in Hcompata.
             rewrite big_op_app in Hcompata *; auto.
           }
           
           assert (j < length t1 (length t1 < j j length (t1 ++ r1 :: t2))
                   j length (t1 ++ r2 :: t2)) as [Hshort | [(Hmid1&Hmid2) | Hlong]].
           { simpl. rewrite ?app_length //=. omega. }
           *** rewrite ?interp_flatten_map.
               unfold interp_flat_map. rewrite Heqa Heqb.
               rewrite ?map_app.
               rewrite ?app_nth1; try (rewrite ?map_length; auto; rewrite -?Hlen1 -?Hlen2; omega).
               erewrite (map_tids_vc); eauto.
           *** rewrite ?interp_flatten_map.
               rewrite ?app_length //= in Hmid2.
               unfold interp_flat_map. rewrite Heqa Heqb.
               rewrite ?map_app.
               rewrite ?app_nth2; try (rewrite ?map_length; auto; rewrite -?Hlen1 -?Hlen2; omega).
               rewrite ?map_length.
               rewrite Hlen1.
               assert ( n', j - length t1' = S n') as (n'&Heq_n').
               {
                 assert (j - length t1' O) as Hne by omega.
                 destruct (j - length t1'); first exfalso; auto.
                 eexists; eauto.
               }
               rewrite Heq_n'. simpl.
               erewrite (map_tids_vc); eauto.
               rewrite ?map_length. clear -Hmid1.
               eapply not_lt. intro Hfalse.
               assert (length t1 < length t1) as Hfalse'. etransitivity; eauto.
               inversion Hfalse'; omega.
           *** rewrite ?interp_flatten_map.
               unfold interp_flat_map. rewrite Heqa Heqb.
               rewrite ?app_length //= in Hlong.
               rewrite ?nth_overflow; auto;
               rewrite ?map_length //= ?app_length //= -?Hlen1 -?Hlen2; auto.
        ** intros j Hlen.
           assert (length t1 = length t1') as Hlen1.
           { rewrite Hequiv1; auto. }
           assert (length t2 = length t2') as Hlen2.
           { rewrite Hequiv2; auto. }
           
           assert ( big_op t1) as Hvalt1.
           { destruct a as [sva Hcompata ? ? ?].
             simpl in ×. clear -Heqa Hcompata. rewrite Heqa in Hcompata.
             rewrite big_op_app in Hcompata *; auto.
           }
           assert ( big_op t2) as Hvalt2.
           { destruct a as [sva Hcompata ? ? ?].
             simpl in ×. clear -Heqa Hcompata. rewrite Heqa in Hcompata.
             rewrite big_op_app in Hcompata *; auto.
           }
           
           assert (j < length t1 (length t1 < j j < length (t1 ++ r1 :: t2))
                   j = length (t1 ++ r2 :: t2)
                   j S (length (t1 ++ r2 :: t2))) as [Hshort | [(Hmid1&Hmid2) | [ Hlong1 | Hlong2] ]].
           { simpl. rewrite ?app_length //=. omega. }
           *** rewrite ?interp_flatten_map.
               unfold interp_flat_map. rewrite Heqa Heqb.
               rewrite ?map_app.
               rewrite ?app_nth1; try (rewrite ?map_length; auto; rewrite -?Hlen1 -?Hlen2; omega).
               erewrite (map_tids_vc); eauto.
           *** rewrite ?interp_flatten_map.
               rewrite ?app_length //= in Hmid2.
               unfold interp_flat_map. rewrite Heqa Heqb.
               rewrite ?map_app.
               rewrite ?app_nth2; try (rewrite ?map_length; auto; rewrite -?Hlen1 -?Hlen2; omega).
               rewrite ?map_length.
               rewrite Hlen1.
               assert ( n', j - length t1' = S n') as (n'&Heq_n').
               {
                 assert (j - length t1' O) as Hne by omega.
                 destruct (j - length t1'); first exfalso; auto.
                 eexists; eauto.
               }
               rewrite Heq_n'. simpl.
               rewrite ?map_app.
               rewrite app_nth1.
               erewrite (map_tids_vc); eauto.
               **** rewrite ?map_length.
                     eapply lt_S_n.
                     rewrite -Heq_n'. rewrite -Hlen1 -Hlen2.
                     omega.
               **** rewrite ?map_length.
                    eapply not_lt. intro Hfalse.
                    assert (length t1 < length t1) as Hfalse'. etransitivity; eauto.
                    inversion Hfalse'; omega.
           *** rewrite ?interp_flatten_map.
               unfold interp_flat_map. rewrite Heqa Heqb.
               rewrite nth_overflow.
               set_unfold. intros; exfalso; auto.

               rewrite ?map_length ?app_length //= in Hlong1 ×.
               rewrite Hlong1. auto.
           *** rewrite ?interp_flatten_map.
               unfold interp_flat_map. rewrite Heqa Heqb.
               rewrite ?nth_overflow; auto.
               **** rewrite ?map_length ?app_length //= ?app_length //= in Hlong2 ×.
                    rewrite -Hlen1 -Hlen2. omega.
               **** rewrite ?map_length ?app_length //= ?app_length //= in Hlong2 ×.
                    eapply le_Sn_le. eauto.
      × rewrite -Heq_ifx'. trf.
        eapply fair_pres_trans; eauto.
        eapply fair_pres_trans; eauto.
  Qed.

End refine_raw_adequacy.