Lemma fold_right_spec P I (f a l : val) xs :
  {{{
    isList l xs ∗ ([∗ list] x ∈ xs, P x) ∗ I [] a ∗
    (∀ (x a' : val) ys,
      {{{ P x ∗ I ys a' }}} f x a' {{{ r, RET r; I (x :: ys) r }}})
  }}}
    fold_right f a l
  {{{ r, RET r; isList l xs ∗ I xs r}}}.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, a, l: val
xs: list val
⟬*PRE@⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭*⟭
fold_right f a l⟬*POST@r,RETr;⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆
I xs r⟭*⟭
Proof.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, a, l: val
xs: list val
⟬*PRE@⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭*⟭
fold_right f a l⟬*POST@r,RETr;⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆
I xs r⟭*⟭
  revert a l.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f: val
xs: list val
∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
  induction xs as [|x xs IHxs].
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f: val
∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ [] ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈[]┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ [] ⟧⟭┆I [] r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ x :: xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x0∈
  x :: xs┆P x0⟭┆⟬Star┆I [] a┆⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r,RETr;I (x0 :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ x :: xs ⟧⟭┆I (x :: xs) r⟭┆
  Φ r⟭⟭⟭┆WP fold_right f a l {{ v, Φ v }}⟭⟭
  all: simpl.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f: val
∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬Pure┆l = InjLV ⟦$LitV┆()%V⟧⟭┆⟬Star┆emp┆⟬Star┆
  I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆f x a'┆⟬Star┆
  P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Pure┆
  l = InjLV ⟦$LitV┆()%V⟧⟭┆I [] r⟭┆Φ r⟭⟭⟭┆WP fold_right f a l {{ v, Φ v }}⟭⟭
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬Exist┆hd┆⟬Exist┆l'┆⟬Star┆⟬Pure┆l = InjRV ⟦$LitV┆hd⟧⟭┆⟬Star┆⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆
  DfracOwn 1 ⟭┆⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆⟬Star┆⟬Star┆
  P x┆⟬BigOp┆∗┆x0∈xs┆P x0⟭⟭┆⟬Star┆I [] a┆⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r,RETr;I (x0 :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Exist┆hd┆⟬Exist┆l'┆⟬Star┆⟬Pure┆
  l = InjRV ⟦$LitV┆hd⟧⟭┆⟬Star┆⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆
  DfracOwn 1 ⟭┆⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
  I (x :: xs) r⟭┆Φ r⟭⟭⟭┆WP fold_right f a l {{ v, Φ v }}⟭⟭
(* BEGIN SOLUTION *)
  -
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f: val
∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬Pure┆l = InjLV ⟦$LitV┆()%V⟧⟭┆⟬Star┆emp┆⟬Star┆
  I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆f x a'┆⟬Star┆
  P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Pure┆
  l = InjLV ⟦$LitV┆()%V⟧⟭┆I [] r⟭┆Φ r⟭⟭⟭┆WP fold_right f a l {{ v, Φ v }}⟭⟭ iIntros (a l) "%Φ (-> & _ & I & #Hf) HΦ".
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, a: val
Φ: val → iPropI Σ
⟬*PRE@"Hf":⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"I":I [] a*⟭
⟬*PRE@"HΦ":⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Pure┆
InjLV ⟦$LitV┆()%V⟧ = InjLV ⟦$LitV┆()%V⟧⟭┆I [] r⟭┆Φ r⟭⟭⟭*⟭
--------------------------------------∗
WP fold_right f a (InjLV ⟦$LitV┆()%V⟧) {{ v, Φ v }}
    wp_rec.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, a: val
Φ: val → iPropI Σ
⟬*PRE@"Hf":⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"I":I [] a*⟭
⟬*PRE@"HΦ":⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Pure┆InjLV ⟦$LitV┆()%V⟧ =
                                       InjLV ⟦$LitV┆()%V⟧⟭┆
I [] r⟭┆Φ r⟭⟭*⟭
--------------------------------------∗
WP (let: "v" := a in
    λ: "l",
      match: "l" with
        InjL <> => "v"
      | InjR "hd" =>
        let: "x" := Fst ! "hd" in
        let: "l'" := Snd ! "hd" in f "x" (fold_right f "v" "l'")
      end) (InjLV ⟦$LitV┆()%V⟧)
{{ v, Φ v }}
    wp_pures.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, a: val
Φ: val → iPropI Σ
⟬*PRE@"Hf":⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"I":I [] a*⟭
⟬*PRE@"HΦ":⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Pure┆InjLV ⟦$LitV┆()%V⟧ =
                                       InjLV ⟦$LitV┆()%V⟧⟭┆
I [] r⟭┆Φ r⟭⟭*⟭
--------------------------------------∗
|={⊤}=> Φ a
    iModIntro.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, a: val
Φ: val → iPropI Σ
⟬*PRE@"Hf":⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"I":I [] a*⟭
⟬*PRE@"HΦ":⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Pure┆InjLV ⟦$LitV┆()%V⟧ =
                                       InjLV ⟦$LitV┆()%V⟧⟭┆
I [] r⟭┆Φ r⟭⟭*⟭
--------------------------------------∗
Φ a
    iApply "HΦ".
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, a: val
Φ: val → iPropI Σ
⟬*PRE@"Hf":⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"I":I [] a*⟭
--------------------------------------∗
⟬Star┆⟬Pure┆InjLV ⟦$LitV┆()%V⟧ = InjLV ⟦$LitV┆()%V⟧⟭┆
I [] a⟭
    by iFrame.
  -
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬Exist┆hd┆⟬Exist┆l'┆⟬Star┆⟬Pure┆l = InjRV ⟦$LitV┆hd⟧⟭┆⟬Star┆⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆
  DfracOwn 1 ⟭┆⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆⟬Star┆⟬Star┆
  P x┆⟬BigOp┆∗┆x0∈xs┆P x0⟭⟭┆⟬Star┆I [] a┆⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r,RETr;I (x0 :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Exist┆hd┆⟬Exist┆l'┆⟬Star┆⟬Pure┆
  l = InjRV ⟦$LitV┆hd⟧⟭┆⟬Star┆⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆
  DfracOwn 1 ⟭┆⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
  I (x :: xs) r⟭┆Φ r⟭⟭⟭┆WP fold_right f a l {{ v, Φ v }}⟭⟭ iIntros (a l) "%Φ ((%hd & %l' & -> & Hhd & Hl) & [P0 Ps] & I & #Hf) HΦ".
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l': val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r,RETr;I (x0 :: ys) r⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"Hl":⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭*⟭
⟬*PRE@"P0":P x*⟭
⟬*PRE@"Ps":⟬BigOp┆∗┆x0∈xs┆P x0⟭*⟭
⟬*PRE@"I":I [] a*⟭
⟬*PRE@"HΦ":⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Exist┆hd0┆⟬Exist┆l'0┆⟬Star┆⟬Pure┆
InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd0⟧⟭┆⟬Star┆⟬PointsTo┆hd0┆⟦$Pair┆x┆l'0⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l'0 ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
I (x :: xs) r⟭┆Φ r⟭⟭⟭*⟭
--------------------------------------∗
WP fold_right f a (InjRV ⟦$LitV┆hd⟧) {{ v, Φ v }}
    wp_rec.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l': val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r,RETr;I (x0 :: ys) r⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"Hl":⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭*⟭
⟬*PRE@"P0":P x*⟭
⟬*PRE@"Ps":⟬BigOp┆∗┆x0∈xs┆P x0⟭*⟭
⟬*PRE@"I":I [] a*⟭
⟬*PRE@"HΦ":⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Exist┆hd0┆⟬Exist┆l'0┆⟬Star┆⟬Pure┆
InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd0⟧⟭┆⟬Star┆⟬PointsTo┆hd0┆⟦$Pair┆x┆l'0⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l'0 ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
I (x :: xs) r⟭┆Φ r⟭⟭*⟭
--------------------------------------∗
WP (let: "v" := a in
    λ: "l",
      match: "l" with
        InjL <> => "v"
      | InjR "hd" =>
        let: "x" := Fst ! "hd" in
        let: "l'" := Snd ! "hd" in f "x" (fold_right f "v" "l'")
      end) (InjRV ⟦$LitV┆hd⟧)
{{ v, Φ v }}
    wp_pures.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l': val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r,RETr;I (x0 :: ys) r⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"Hl":⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭*⟭
⟬*PRE@"P0":P x*⟭
⟬*PRE@"Ps":⟬BigOp┆∗┆x0∈xs┆P x0⟭*⟭
⟬*PRE@"I":I [] a*⟭
⟬*PRE@"HΦ":⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Exist┆hd0┆⟬Exist┆l'0┆⟬Star┆⟬Pure┆
InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd0⟧⟭┆⟬Star┆⟬PointsTo┆hd0┆⟦$Pair┆x┆l'0⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l'0 ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
I (x :: xs) r⟭┆Φ r⟭⟭*⟭
--------------------------------------∗
WP let: "x" := Fst ! ⟦$LitV┆hd⟧ in
   let: "l'" := Snd ! ⟦$LitV┆hd⟧ in f "x" (fold_right f a "l'")
{{ v, Φ v }}
    wp_load.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l': val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r,RETr;I (x0 :: ys) r⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"Hl":⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭*⟭
⟬*PRE@"P0":P x*⟭
⟬*PRE@"Ps":⟬BigOp┆∗┆x0∈xs┆P x0⟭*⟭
⟬*PRE@"I":I [] a*⟭
⟬*PRE@"HΦ":⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Exist┆hd0┆⟬Exist┆l'0┆⟬Star┆⟬Pure┆
InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd0⟧⟭┆⟬Star┆⟬PointsTo┆hd0┆⟦$Pair┆x┆l'0⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l'0 ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
I (x :: xs) r⟭┆Φ r⟭⟭*⟭
--------------------------------------∗
WP let: "x" := Fst (x, l')%V in
   let: "l'" := Snd ! ⟦$LitV┆hd⟧ in f "x" (fold_right f a "l'")
{{ v, Φ v }}
    wp_load.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l': val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r,RETr;I (x0 :: ys) r⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"Hl":⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭*⟭
⟬*PRE@"P0":P x*⟭
⟬*PRE@"Ps":⟬BigOp┆∗┆x0∈xs┆P x0⟭*⟭
⟬*PRE@"I":I [] a*⟭
⟬*PRE@"HΦ":⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Exist┆hd0┆⟬Exist┆l'0┆⟬Star┆⟬Pure┆
InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd0⟧⟭┆⟬Star┆⟬PointsTo┆hd0┆⟦$Pair┆x┆l'0⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l'0 ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
I (x :: xs) r⟭┆Φ r⟭⟭*⟭
--------------------------------------∗
WP let: "l'" := Snd (x, l')%V in f x (fold_right f a "l'") {{ v, Φ v }}
    wp_pures.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l': val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r,RETr;I (x0 :: ys) r⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"Hl":⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭*⟭
⟬*PRE@"P0":P x*⟭
⟬*PRE@"Ps":⟬BigOp┆∗┆x0∈xs┆P x0⟭*⟭
⟬*PRE@"I":I [] a*⟭
⟬*PRE@"HΦ":⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Exist┆hd0┆⟬Exist┆l'0┆⟬Star┆⟬Pure┆
InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd0⟧⟭┆⟬Star┆⟬PointsTo┆hd0┆⟦$Pair┆x┆l'0⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l'0 ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
I (x :: xs) r⟭┆Φ r⟭⟭*⟭
--------------------------------------∗
WP f x (fold_right f a l') {{ v, Φ v }}
    wp_apply (IHxs with "[$Hl $Ps $I $Hf]").
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l': val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r,RETr;I (x0 :: ys) r⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"P0":P x*⟭
⟬*PRE@"HΦ":⟬Forall┆r┆⟬Wand┆⟬Star┆⟬Exist┆hd0┆⟬Exist┆l'0┆⟬Star┆⟬Pure┆
InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd0⟧⟭┆⟬Star┆⟬PointsTo┆hd0┆⟦$Pair┆x┆l'0⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l'0 ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
I (x :: xs) r⟭┆Φ r⟭⟭*⟭
--------------------------------------∗
⟬Forall┆r┆⟬Wand┆⟬Star┆⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭┆
I xs r⟭┆WP f x r {{ v, Φ v }}⟭⟭
    iIntros "%r [Hl I]".
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l', r: val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r0,RETr0;I (x0 :: ys) r0⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"P0":P x*⟭
⟬*PRE@"HΦ":⟬Forall┆r0┆⟬Wand┆⟬Star┆⟬Exist┆hd0┆⟬Exist┆l'0┆⟬Star┆⟬Pure┆
InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd0⟧⟭┆⟬Star┆⟬PointsTo┆hd0┆⟦$Pair┆x┆l'0⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l'0 ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
I (x :: xs) r0⟭┆Φ r0⟭⟭*⟭
⟬*PRE@"Hl":⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭*⟭
⟬*PRE@"I":I xs r*⟭
--------------------------------------∗
WP f x r {{ v, Φ v }}
    wp_apply ("Hf" with "[$P0 $I]").
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l', r: val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r0,RETr0;I (x0 :: ys) r0⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"HΦ":⟬Forall┆r0┆⟬Wand┆⟬Star┆⟬Exist┆hd0┆⟬Exist┆l'0┆⟬Star┆⟬Pure┆
InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd0⟧⟭┆⟬Star┆⟬PointsTo┆hd0┆⟦$Pair┆x┆l'0⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l'0 ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
I (x :: xs) r0⟭┆Φ r0⟭⟭*⟭
⟬*PRE@"Hl":⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭*⟭
--------------------------------------∗
⟬Forall┆r0┆⟬Wand┆I (x :: xs) r0┆Φ r0⟭⟭
    iIntros "%r' I".
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l', r, r': val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r0,RETr0;I (x0 :: ys) r0⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"HΦ":⟬Forall┆r0┆⟬Wand┆⟬Star┆⟬Exist┆hd0┆⟬Exist┆l'0┆⟬Star┆⟬Pure┆
InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd0⟧⟭┆⟬Star┆⟬PointsTo┆hd0┆⟦$Pair┆x┆l'0⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l'0 ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
I (x :: xs) r0⟭┆Φ r0⟭⟭*⟭
⟬*PRE@"Hl":⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭*⟭
⟬*PRE@"I":I (x :: xs) r'*⟭
--------------------------------------∗
Φ r'
    iApply "HΦ".
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l', r, r': val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r0,RETr0;I (x0 :: ys) r0⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"Hl":⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭*⟭
⟬*PRE@"I":I (x :: xs) r'*⟭
--------------------------------------∗
⟬Star┆⟬Exist┆hd0┆⟬Exist┆l'0┆⟬Star┆⟬Pure┆InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd0⟧⟭┆⟬Star┆⟬PointsTo┆hd0┆⟦$Pair┆x┆l'0⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l'0 ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭┆
I (x :: xs) r'⟭
    iFrame "I".
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l', r, r': val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r0,RETr0;I (x0 :: ys) r0⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"Hl":⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭*⟭
--------------------------------------∗
⟬Exist┆hd0┆⟬Exist┆l'0┆⟬Star┆⟬Pure┆InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd0⟧⟭┆⟬Star┆⟬PointsTo┆hd0┆⟦$Pair┆x┆l'0⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l'0 ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭⟭⟭
    iExists hd, l'.
Σ: gFunctors
heapGS0: heapGS Σ
P: val → iPropI Σ
I: list val → val → iPropI Σ
f, x: val
xs: list val
IHxs: ∀ (a l : val) (Φ : val → iPropI Σ),
  ⟬Wand┆⟬Star┆⟬PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆⟬Star┆⟬BigOp┆∗┆x∈xs┆
  P x⟭┆⟬Star┆I [] a┆⟬Forall┆x┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
  f x a'┆⟬Star┆P x┆I ys a'⟭┆r,RETr;I (x :: ys) r⟭⟭⟭⟭⟭⟭⟭┆⟬Wand┆⟬Modality┆▷┆⟬Forall┆r┆⟬Wand┆⟬Star┆⟬
  PointsTo ┆ l ┆ ⟦ isList ┆ xs ⟧⟭┆I xs r⟭┆Φ r⟭⟭⟭┆WP 
                                                 fold_right f a l
                                                 {{ 
                                                 v, Φ v }}⟭⟭
a: val
Φ: val → iPropI Σ
hd: loc
l', r, r': val
⟬*PRE@"Hf":⟬Forall┆x0┆⟬Forall┆a'┆⟬Forall┆ys┆⟬Triple┆
f x0 a'┆⟬Star┆P x0┆I ys a'⟭┆r0,RETr0;I (x0 :: ys) r0⟭⟭⟭⟭*⟭
--------------------------------------□
⟬*PRE@"Hhd":⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆DfracOwn 1 ⟭*⟭
⟬*PRE@"Hl":⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭*⟭
--------------------------------------∗
⟬Star┆⟬Pure┆InjRV ⟦$LitV┆hd⟧ = InjRV ⟦$LitV┆hd⟧⟭┆⟬Star┆⟬PointsTo┆hd┆⟦$Pair┆x┆l'⟧┆
DfracOwn 1 ⟭┆⟬PointsTo ┆ l' ┆ ⟦ isList ┆ xs ⟧⟭⟭⟭
    by iFrame.
Qed.