Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslmodel fslassnlemmas.
Require Import fslhmap.

Set Implicit Arguments.

Lemma step_back_from_normal:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge))
    hf (MAP: hmap edge = Hdef hf) l (LAB: HVlabeled (hf l) HLnormal) (ALL: hf l ≠ HVnone),
  << ALLOC: lab (hb_fst edge) = Aalloc l >> ∨
  ∃ edge´ hf´, << CON: hb_snd edge´ = Some (hb_fst edge) >> ∧ << EV´: edge_valid lab sb rf edge´ >> ∧
                    << MAP´: hmap edge´ = Hdef hf´ >> ∧ << ALL´: hf´ l ≠ HVnone >> ∧ << SB: ¬ is_rf edge >> ∧
                   (<< SB´: is_sb edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLnormal >> ∨
                    << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLnabla >> ∧
                                              << ACQ: is_acquire_fence (lab (hb_fst edge)) >> ∨
                    << RF´: is_rf edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLnabla >> ∧
                                              << ACQ: is_acquire_read (lab (hb_fst edge)) >>).
Proof.
  ins; unnw.
  unfold hmap_valid, unique in VALID.
  desfh; desc; try (destruct DISJ; desc); destruct edge; ins; try revert TYP; desfh;
    try (by red in EV; rewrite Heq in EV);
    try (by specialize (CONS_RF e´); desfh; desfh; rewrite Heq in *; desfh);
    rewrite ?(qU0 _ EV), ?MAP in *; desfh;
    try (by inv sEQ);
    try (by rewrite rEQ in MAP; inv MAP).

  {
    right.
    symmetry in qEQ; assert (D := (hplus_def_inv_l _ _ qEQ)); desfh.
    rewrite D in ×.
    symmetry in D; eapply hsum_preserves_label in D; eauto; desfh.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply qOK.
    symmetry in qEQ; eapply hplus_preserves_label in qEQ; eauto; desfh.
    assert (pEQ´ := pEQ).
    symmetry in pEQ; eapply hsum_preserves_label_inv in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    right.
    symmetry in qEQ; rewrite hplusC in qEQ; assert (D := (hplus_def_inv_l _ _ qEQ)); desfh.
    symmetry in qEQ; eapply hplus_preserves_label in qEQ; eauto; desfh.
    symmetry in pEQ; eapply hsum_preserves_label_inv in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    destruct (classic (l = l0)); eauto.
    right; eexists (hb_sb _ e), _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
  }

  {
    destruct (classic (l = l0)); eauto.
    right; eexists (hb_sb _ e), _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
  }

  {
    right.
    rewrite pEQ in qEQ; inv qEQ.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    right; revert TYP.
    symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
    × unfold hupd in qEQ0, qEQ1; desfh; desfh.
      symmetry in pEQ´; eapply hplus_preserves_label in pEQ´; rewrite ?hupds; try by eauto.
      desfh; eexists (hb_sb _ e), _; repeat split; ins; eauto.
    × eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
      + red in TRAN; desfh.
        rewrite TRAN in ×.
        assert (A := Hsim_alloc l rfsSIM qEQ3); desfh.
        red in rfsSIM; desfh.
        specialize (rfsSIM1 l).
        rewrite HVsim_sym in rfsSIM1; eapply label_sim in rfsSIM1; eauto; desfh.
        specialize (TRAN3 l).
        exploit label_is_consistent_with_exact_label; eauto; intro; desfh.
        symmetry in TRAN; eapply hsum_preserves_label_inv in TRAN; eauto; desfh.
        repeat (rewrite In_map in *; desfh).
        eexists (hb_rf _ e), _; ins; repeat split; eauto.
          by apply rfsOK.
        repeat right; repeat split; desfh.
        - red in TYP; desfh; specialize (TYP0 l).
          by exploit label_is_consistent_with_exact_label; eauto.
        - desf.
      + symmetry in pEQ´; rewrite hplusC in pEQ´; eapply hplus_preserves_label in pEQ´; eauto; desfh.
        eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    right; clear TYP.
    unfold hupd in ALL; desfh; desfh.
    symmetry in pEQ´; eapply hplus_preserves_label in pEQ´; rewrite ?hupds; simpls; desfh.
      2: by instantiate (1 := HLnormal); vauto.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    right; eexists (hb_sb _ e), _; repeat split; ins; eauto.
    × unfold hupd in ALL; desf; desf.
      by intro N; rewrite N in IV; ins.
    × left; intuition.
      unfold hupd in LAB; desf; desf.
      red; desf; ins; desf.
  }

  {
    right; clear TYP.
    destruct (classic (l = l0)).
    × subst l0.
      eapply hplus_preserves_Wlabel in qEQ; rewrite ?hupds; simpls; desfh.
        2: by instantiate (1 := HLnormal); vauto.
      eapply hplus_preserves_Wlabel in UPD; eauto; desfh.
      apply initialize_Wlabel in UPD.
      assert (hf0 l ≠ HVnone) by (intro U; rewrite U in *; ins).
      apply Wlabel_implies_label in UPD.
      eexists (hb_sb _ e), _; repeat split; ins; eauto.
    × eapply hplus_preserves_label in UPD; eauto; desfh.
      rewrite <- initialize_alloc in UPD.
      unfold initialize, hupd in UPD0; desfh.
      eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    exfalso.
    red in TRAN; desfh.
    rewrite TRAN in ×.
    assert (R := hplus_def_inv_l _ _ TRAN); desf.
    rewrite R in ×.
    symmetry in R; eapply hsum_preserves_label in R; eauto; desf.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply rfsOK.
    symmetry in TRAN; eapply hplus_preserves_label in TRAN; eauto; desf.
    specialize (TRAN3 l).
    by exploit label_is_consistent_with_exact_label; eauto.
  }

  {
    exfalso.
    red in TRAN; desfh.
    symmetry in TRAN; rewrite hplusC in TRAN; eapply hplus_preserves_label in TRAN; eauto; desf.
    specialize (TRAN3 l).
    by exploit label_is_consistent_with_exact_label; eauto.
  }

  {
    rewrite hdef_alt in DEF; desfh.
    rewrite DEF in ×.
    right; eexists (hb_sb _ e), _; do 3 (split; eauto).
    symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
      by eapply hplus_preserves_label in pEQ; eauto; desfh; ins; intuition.
    eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
    × exfalso; red in RELlabel´; desf.
      specialize (RELlabel´0 l).
      by exploit label_is_consistent_with_exact_label; eauto.
    × red in ACQsim; desfh.
      specialize (ACQsim1 l).
      rewrite <- HVsim_alloc in qEQ3; eauto.
      rewrite HVsim_sym in ACQsim1.
      eapply label_sim in ACQsim1; eauto; desfh.
      red in ACQlabel; desfh.
      specialize (ACQlabel0 l).
      exploit label_is_consistent_with_exact_label; eauto; ins; desfh.
      rewrite <- hplusA, hplusC in pEQ.
      eapply hplus_preserves_label in pEQ; eauto; desfh; intuition.
      right; left; intuition; desf; intuition.
      inv H; intuition.
  }
Qed.

Lemma step_back_from_nabla:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge))
    hf (MAP: hmap edge = Hdef hf) l (LAB: HVlabeled (hf l) HLnabla) (ALL: hf l ≠ HVnone),
  ∃ edge´ hf´, << CON: hb_snd edge´ = Some (hb_fst edge) >> ∧ << EV´: edge_valid lab sb rf edge´ >> ∧
                    << MAP´: hmap edge´ = Hdef hf´ >> ∧ << ALL´: hf´ l ≠ HVnone >> ∧
                   (<< SB: ¬ is_rf edge >> ∧ << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLnabla >> ∨
                    << SB: ¬ is_rf edge >> ∧ << RF´: is_rf edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLnabla >> ∨
                    << RF: ¬ is_sb edge >> ∧ << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLtriangle >> ∨
                    << RF: ¬ is_sb edge >> ∧ << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeled (hf´ l) HLnormal >> ∧
                                              << REL: is_release_write (lab (hb_fst edge)) >>).
Proof.
  ins; unnw.
  unfold hmap_valid, unique in VALID.
  desfh; desc; try (destruct DISJ; desc); destruct edge; ins; try revert TYP; desfh;
    try (by red in EV; rewrite Heq in EV);
    try (by specialize (CONS_RF e´); desfh; desfh; rewrite Heq in *; desfh);
    rewrite ?(qU0 _ EV), ?MAP in *; desfh;
    try (by inv sEQ);
    try (by rewrite rEQ in MAP; inv MAP).

  {
    symmetry in qEQ; assert (D := (hplus_def_inv_l _ _ qEQ)); desfh.
    rewrite D in ×.
    symmetry in D; eapply hsum_preserves_label in D; eauto; desfh.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply qOK.
    symmetry in qEQ; eapply hplus_preserves_label in qEQ; eauto; desfh.
    assert (pEQ´ := pEQ).
    symmetry in pEQ; eapply hsum_preserves_label_inv in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    symmetry in qEQ; rewrite hplusC in qEQ; assert (D := (hplus_def_inv_l _ _ qEQ)); desfh.
    symmetry in qEQ; eapply hplus_preserves_label in qEQ; eauto; desfh.
    symmetry in pEQ; eapply hsum_preserves_label_inv in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    eexists (hb_sb _ e), _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
  }

  {
    eexists (hb_sb _ e), _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto;
      ins; unfold is_nabla in LAB; desf.
  }

  {
    rewrite pEQ in qEQ; inv qEQ.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
    × exfalso.
      unfold hupd in qEQ0, qEQ1; desf; ins; desfh.
      unfold is_nabla in qEQ0; desf.
    × eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
      + red in TRAN; desfh.
        rewrite TRAN in ×.
        assert (A := Hsim_alloc l rfsSIM qEQ3); desfh.
        red in rfsSIM; desfh.
        specialize (rfsSIM1 l).
        rewrite HVsim_sym in rfsSIM1; eapply label_sim in rfsSIM1; eauto; desfh.
        specialize (TRAN3 l).
        exploit label_is_consistent_with_exact_label; eauto; intro; desfh.
        symmetry in TRAN; eapply hsum_preserves_label_inv in TRAN; eauto; desfh.
        repeat (rewrite In_map in *; desfh).
        eexists (hb_rf _ e), _; ins; repeat split; eauto 6.
        by apply rfsOK.
      + symmetry in pEQ´; rewrite hplusC in pEQ´; eapply hplus_preserves_label in pEQ´; eauto; desfh.
        eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    exfalso.
    unfold hupd in *; desf; desf; eauto; ins; unfold is_nabla in LAB; desf.
  }

  {
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    × unfold hupd in ALL; desf; desf.
      by intro N; rewrite N in IV; ins.
    × left; intuition.
      unfold hupd in LAB; desf; desf.
  }

  {
    eapply hplus_preserves_label in UPD; eauto; desfh.
    rewrite <- initialize_alloc in UPD.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    clear TYP; left; intuition.
    by eapply initialize_not_normal; eauto.
  }

  {
    eexists (hb_sb _ e), _; do 3 (split; eauto).
    revert TYP.
    red in TRAN; desfh.
    rewrite TRAN in ×.
    assert (R := hplus_def_inv_l _ _ TRAN); desfh.
    rewrite R in ×.
    symmetry in R; eapply hsum_preserves_label in R; eauto; desfh.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply rfsOK.
    symmetry in TRAN; eapply hplus_preserves_label in TRAN; eauto; desfh.
    red in rfsSIM; desfh.
    specialize (rfsSIM1 l).
    rewrite HVsim_alloc in TRAN; eauto.
    eapply label_sim in rfsSIM1; eauto; desfh.
    assert (UPDcopy := UPD).
    rewrite hplusC in UPD; eapply hplus_preserves_label in UPD; eauto; desfh.
    rewrite <- initialize_alloc in UPD.
    ins; desfh.
    × red in TYP; desfh.
      specialize (TYP0 l); exploit label_is_consistent_with_exact_label; eauto; intro; desfh.
      intuition.
      right; right; left; intuition.
      by eapply initialize_not_normal; eauto.
    × red in TYP1; desfh.
      specialize (TYP2 l); exploit label_is_consistent_with_exact_label; eauto; intro; desfh.
      intuition.
      repeat right; intuition; desf; intuition.
      destruct (classic (l = l0)).
      + subst l0.
        rewrite qEQ, hplusA in UPDcopy.
        eapply hplus_preserves_Wlabel in UPDcopy; rewrite ?hupds; simpls; desfh.
          2: by instantiate (1 := HLnormal); vauto.
        by apply initialize_Wlabel, Wlabel_implies_label in UPDcopy.
      + by unfold initialize, hupd in UPD0; ins; desf.
  }

  {
    eexists (hb_sb _ e), _; do 3 (split; eauto).
    revert TYP.
    red in TRAN; desfh.
    rewrite TRAN in ×.
    symmetry in TRAN; rewrite hplusC in TRAN; eapply hplus_preserves_label in TRAN; eauto; desfh.
    red in rfsSIM; desfh.
    specialize (rfsSIM1 l).
    rewrite HVsim_alloc in TRAN; eauto.
    eapply label_sim in rfsSIM1; eauto; desfh.
    assert (UPDcopy := UPD).
    rewrite hplusC in UPD; eapply hplus_preserves_label in UPD; eauto; desfh.
    rewrite <- initialize_alloc in UPD.
    ins; desfh.
    × red in TYP; desfh.
      specialize (TYP0 l); exploit label_is_consistent_with_exact_label; eauto; intro; desfh.
      intuition.
      right; right; left; intuition.
      by eapply initialize_not_normal; eauto.
    × red in TYP1; desfh.
      specialize (TYP2 l); exploit label_is_consistent_with_exact_label; eauto; intro; desfh.
      intuition.
      repeat right; intuition; desf; intuition.
      destruct (classic (l = l0)).
      + subst l0.
        rewrite qEQ, hplusA in UPDcopy.
        eapply hplus_preserves_Wlabel in UPDcopy; rewrite ?hupds; simpls; desfh.
          2: by instantiate (1 := HLnormal); vauto.
        by apply initialize_Wlabel, Wlabel_implies_label in UPDcopy.
      + by unfold initialize, hupd in UPD0; ins; desf.
  }

  {
    rewrite hdef_alt in DEF; desfh.
    rewrite DEF in ×.
    eexists (hb_sb _ e), _; do 3 (split; eauto).
    symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
      by eapply hplus_preserves_label in pEQ; eauto; desfh; ins; intuition.
    eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
    × exfalso; red in RELlabel´; desf.
      specialize (RELlabel´0 l).
      by exploit label_is_consistent_with_exact_label; eauto.
    × exfalso; red in ACQlabel´; desf.
      specialize (ACQlabel´0 l).
      by exploit label_is_consistent_with_exact_label; eauto.
  }
Qed.

Lemma step_back_from_triangle:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge))
    hf (MAP: hmap edge = Hdef hf) l (LAB: HVlabeled (hf l) HLtriangle) (ALL: hf l ≠ HVnone),
  ∃ edge´ hf´, << CON: hb_snd edge´ = Some (hb_fst edge) >> ∧ << EV´: edge_valid lab sb rf edge´ >> ∧
                    << MAP´: hmap edge´ = Hdef hf´ >> ∧ << ALL´: hf´ l ≠ HVnone >> ∧
                    << SB: ¬ is_rf edge >> ∧ << SB´: is_sb edge´ >> ∧
                   (<< LAB´: HVlabeled (hf´ l) HLtriangle >> ∨
                    << LAB´: HVlabeled (hf´ l) HLnormal >> ∧ << REL: is_release_fence (lab (hb_fst edge)) >>).
Proof.
  ins; unnw.
  unfold hmap_valid, unique in VALID.
  desfh; desc; try (destruct DISJ; desc); destruct edge; ins; try revert TYP; desfh;
    try (by red in EV; rewrite Heq in EV);
    try (by specialize (CONS_RF e´); desfh; desfh; rewrite Heq in *; desfh);
    rewrite ?(qU0 _ EV), ?MAP in *; desfh;
    try (by inv sEQ);
    try (by rewrite rEQ in MAP; inv MAP).

  {
    symmetry in qEQ; assert (D := (hplus_def_inv_l _ _ qEQ)); desfh.
    rewrite D in ×.
    symmetry in D; eapply hsum_preserves_label in D; eauto; desfh.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply qOK.
    symmetry in qEQ; eapply hplus_preserves_label in qEQ; eauto; desfh.
    assert (pEQ´ := pEQ).
    symmetry in pEQ; eapply hsum_preserves_label_inv in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    symmetry in qEQ; rewrite hplusC in qEQ; assert (D := (hplus_def_inv_l _ _ qEQ)); desfh.
    symmetry in qEQ; eapply hplus_preserves_label in qEQ; eauto; desfh.
    symmetry in pEQ; eapply hsum_preserves_label_inv in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    eexists (hb_sb _ e), _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
  }

  {
    eexists (hb_sb _ e), _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto;
      ins; unfold is_triangle in LAB; desf.
  }

  {
    rewrite pEQ in qEQ; inv qEQ.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
    × exfalso.
      unfold hupd in qEQ0, qEQ1; desf; ins; desfh.
      unfold is_triangle in qEQ0; desf.
    × eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
      + ins; exfalso.
        assert (L: ∃ lbl, HlabeledExact (Hdef hf´0) lbl ∧ lbl ≠ HLtriangle) by (by desf; eexists,; eauto).
        clear TYP; desf.
        red in L; desf.
        specialize (L1 l); exploit label_is_consistent_with_exact_label; eauto; intro; desf.
      + symmetry in pEQ´; rewrite hplusC in pEQ´; eapply hplus_preserves_label in pEQ´; eauto; desfh.
        eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    exfalso.
    unfold hupd in *; desf; desf; eauto; ins; unfold is_triangle in LAB; desf.
  }

  {
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    × unfold hupd in ALL; desf; desf.
      by intro N; rewrite N in IV; ins.
    × left; intuition.
      unfold hupd in LAB; desf; desf.
  }

  {
    eapply hplus_preserves_label in UPD; eauto; desfh.
    rewrite <- initialize_alloc in UPD.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    clear TYP; left; intuition.
    by eapply initialize_not_normal; eauto.
  }

  {
    exfalso.
    red in TRAN; desfh.
    assert (R := hplus_def_inv_l _ _ TRAN); desf.
    rewrite R in ×.
    symmetry in R; eapply hsum_preserves_label in R; eauto; desf.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply rfsOK.
    symmetry in TRAN; eapply hplus_preserves_label in TRAN; eauto; desf.
    specialize (TRAN3 l); exploit label_is_consistent_with_exact_label; eauto; intro; desf.
  }

  {
    exfalso.
    red in TRAN; desfh.
    symmetry in TRAN; rewrite hplusC in TRAN; eapply hplus_preserves_label in TRAN; eauto; desf.
    specialize (TRAN3 l); exploit label_is_consistent_with_exact_label; eauto; intro; desf.
  }

  {
    rewrite hdef_alt in DEF; desfh.
    rewrite DEF in ×.
    eexists (hb_sb _ e), _; do 3 (split; eauto).
    symmetry in qEQ; eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
      by eapply hplus_preserves_label in pEQ; eauto; desfh; ins; intuition.
    eapply hplus_preserves_label_inv in qEQ; eauto; desfh.
    × red in RELsim; desfh.
      specialize (RELsim1 l).
      rewrite <- HVsim_alloc in qEQ3; eauto.
      apply HVsim_sym in RELsim1; eapply label_sim in qEQ2; eauto; desfh.
      red in RELlabel; desfh.
      specialize (RELlabel0 l); exploit label_is_consistent_with_exact_label; eauto; desfh.
      rewrite hplusAC in pEQ; eapply hplus_preserves_label in pEQ; eauto; ins; desfh; intuition.
      right; split; try done; desf; intuition.
      inv H; intuition.
    × exfalso; red in ACQlabel´; desf.
      specialize (ACQlabel´0 l).
      by exploit label_is_consistent_with_exact_label; eauto.
  }
Qed.