---
title: "Satisfaction by recursion on formulas"
module: L.Coding.Satisfaction
lang: en
site: "Bedrock"
description: "Satisfaction by recursion on formulas"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 49
canonical: https://bedrock.institute/en/L.Coding.Satisfaction.html
html: L.Coding.Satisfaction.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Satisfaction.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Axioms.Full, L.Coding.Model, L.Coding.Expressions, L.Coding.EnvironmentSet]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.Satisfaction.md, https://bedrock.institute/ja/L.Coding.Satisfaction.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Satisfaction by recursion on formulas

Given a set `B` in `L` and a formula, we construct the set of environments over `B` that satisfy that formula. The construction proceeds by recursion on the formula: for a compound formula the set is determined by the sets of its immediate subformulas, while the atoms and falsity are handled directly. In every case the set is obtained by separation, from the set of all length-`n` environments over `B`, of those whose entries meet a describing condition. The membership equations of the resulting sets describe the ten formula constructors.

The recursion being on a meta-language formula shapes every step. Agda can inspect the formula, so each step may name the sets produced at the subformulas as constants of the describing condition, and the object language never has to quantify over a code. The atoms are correspondingly short: a meta-language term is visibly a variable or a constant, so reading its value has one case rather than the two that a coded clause must distinguish.

```agda
{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Coding.Satisfaction {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

The construction is carried out under excluded middle at the successor of the model level. Its formulas belong to the language of set theory, with equality, membership, the three binary connectives, falsity, and bounded and unbounded quantifiers.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Term; con; var; Formula
        ; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Absoluteness
```

Satisfaction will be read in the constructible substructure of the cumulative hierarchy. Formula absoluteness supplies that restricted reading, while ordered pairs encode the graphs used as environments.

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
```

For each formula, separation cuts its satisfaction set out of the set of coded environments. The formulas `appAt` and `consAtL` describe lookup in an environment graph and extension by one value; `envSet` supplies all environments of the required length.

```agda
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate )
open import L.Coding.Expressions {ℓ} using ( consAtL; numL )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
```

Existential clauses produce propositionally truncated witnesses. Finite indices are converted to natural numbers and then represented by von Neumann numerals inside the hierarchy.

```agda
open import Cubical.Data.FinData using ( toℕ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
```

The hierarchy's numeral construction names those indices as sets. Opening the constructible truth-valued structure fixes the meaning of membership and satisfaction throughout the chapter.

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( #_ )
```

The notation `_⊨_` below is satisfaction in the restricted constructible structure, evaluated under a finite environment vector.

```agda
open hPropStructure 𝒮ʟ

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
```

## Evaluating variables and constants

A variable obtains its value from the environment at its index; a constant already names its value. Both facts are said inside the object language, because the describing conditions are formulas. The term reader `tmIs` says, of a value slot and an environment slot, that the environment assigns to the term the value at the value slot. For a constant this is the bare equation between the value slot and the constant. For a variable it is an existence statement: some carrier element equals the numeral of the index, and the application clause says that the pair of that index and the recorded value belongs to the graph of the environment recorded at the environment slot. Satisfaction judgments throughout are read in `L`.

```agda
private
  nn : ℕ → S
  nn k = # k , numL k
```

The internal numerals pair the ambient von Neumann numerals with their constructibility proofs, so an index can be named inside `L` wherever it is needed.

```agda
tmIs : ∀ {n m} → Term S n → Fin m → Fin m → Formula S m
```

The reader takes a term, the slot holding the value of the term, and the slot holding the environment in which the term is read, and it returns a formula over environments of that length.

```agda
tmIs (var i) v e =
  ∃̇ ((var zero ≐ con (nn (toℕ i))) ∧̇ appAt (suc e) zero (suc v))
```

For a variable, the clause says that some carrier element `x` equals the numeral of the index, and that the pair of that index and the value at the value slot belongs to the graph of the environment recorded at the environment slot. The equation only pins the index witness; the application clause carries the content.

```agda
tmIs (con c) v e = var v ≐ con c
```

For a constant, no environment is consulted: the value slot is simply identified with the constant.

```agda
tmIs-var-in : ∀ {n m} (i : Fin n) (γ : S ^ m) (v e : Fin m)
            → ⟨ pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩
            → ⟨ γ ⊨ tmIs {n} (var i) v e ⟩
```

The adequacy lemmas connect the formula with the ambient membership it encodes. Inward: if the environment at slot `e` contains the pair of the numeral `i` and the value at slot `v`, then `γ` satisfies the reader.

```agda
tmIs-var-in i γ v e h = ∣ nn (toℕ i)
  , ( refl
    , subst ⟨_⟩ (sym (appAt-adequate (suc e) zero (suc v) (nn (toℕ i) ∷ γ))) h ) ∣₁
```

The witness is the numeral itself; its defining equation is definitional, and the membership travels along the adequacy path, read in reverse, from the ambient statement to the internal clause over the extended environment.

```agda
tmIs-var-out : ∀ {n m} (i : Fin n) (γ : S ^ m) (v e : Fin m)
             → ⟨ γ ⊨ tmIs {n} (var i) v e ⟩
             → ⟨ pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩
```

Outward, satisfaction of the reader yields the ambient membership. Here a general principle of the chapter appears for the first time: a truncated witness may be consumed whenever the goal is a proposition or a truncation, and nothing below violates this.

```agda
tmIs-var-out i γ v e = PT.rec
  (snd (pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ)))
```

The truncated witness pairs an entry `x` with the proof that `x` is the numeral of the index and that the clause over the extended environment holds.

```agda
  (λ { (x , (qx , m)) →
    subst (λ w → ⟨ pr w (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩) qx
      (subst ⟨_⟩ (appAt-adequate (suc e) zero (suc v) (x ∷ γ)) m) })
```

The adequacy path identifies the clause with the membership of the pair of `x` and the value; rewriting `x` back to the numeral along its equation leaves exactly the membership that the outward direction owes.

## The set of satisfying environments

For each constructor, a formula describes which environments to retain by separation, and every describing condition is a one-variable formula over environments of the formula's own arity. The connectives refer to the sets already built for the subformulas, naming them as constants. An unbounded quantifier conses a member of the carrier onto the environment and asks whether the extension belongs to the set one arity up; the bounded quantifiers add the second guard that the new entry lies in the bounding term's value. Every step of the construction is thus one separation.

```agda
private
  opaque
    sep : (a : S) → Formula S 1 → S
    sep a φ = hasSeparationL a φ .fst .fst
```

Separation is recorded once, in its opaque wrapper: from a set and a one-variable formula it produces the subset.

```agda
    sep-mem : (a : S) (φ : Formula S 1) (x : S)
            → (x ∈ˢ sep a φ) ≡ ((x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ))
    sep-mem a φ = hasSeparationL a φ .fst .snd
```

The membership specification is the whole content of separation: membership in the subset is membership in the ambient set together with satisfaction of the condition.

```agda
module _ (B : S) where
  cond : ∀ {n} → Formula S n → Formula S 1
```

Fix a base set `B`. Every formula will determine a unary condition on a coded environment over `B`; separating the environments that satisfy this condition produces its satisfaction set.

```agda
  Sat : ∀ {n} → Formula S n → S
  Sat {n} φ = sep (envSet B n) (cond φ)
```

The set of satisfying environments is the separation, from the full environment set at the formula's arity, of the environments meeting the condition.

```agda
  Sat-mem : ∀ {n} (φ : Formula S n) (x : S)
          → (x ∈ˢ Sat φ) ≡ ((x ∈ˢ envSet B n) ⊓ ((x ∷ []) ⊨ cond φ))
  Sat-mem {n} φ = sep-mem (envSet B n) (cond φ)
```

Its membership equation records exactly the two requirements: the environment has the right arity and values, and it meets the condition specific to the formula.

```agda
  cond (t ∈̇ u) =
    (∃̇ (∃̇ ( tmIs t (suc zero) (suc (suc zero))
          ∧̇ ( tmIs u zero (suc (suc zero))
          ∧̇ (var (suc zero) ∈̇ var zero) ))))
```

The membership atom binds two entries and asserts the object-language membership of the value of `t`, read at slot `suc zero`, in the value of `u`, read at slot `zero`. Both values are read against the environment slot.

```agda
  cond (t ≐ u) =
    (∃̇ (∃̇ ( tmIs t (suc zero) (suc (suc zero))
          ∧̇ ( tmIs u zero (suc (suc zero))
          ∧̇ (var (suc zero) ≐ var zero) ))))
```

The equality atom has the same shape with equality in place of membership.

```agda
  cond (a ∧̇ b) =
    ((var zero ∈̇ con (Sat a)) ∧̇ (var zero ∈̇ con (Sat b)))
```

A conjunction's condition asks of the environment that it belong to both subformula sets, each named as a constant.

```agda
  cond (a ∨̇ b) =
    ((var zero ∈̇ con (Sat a)) ∨̇ (var zero ∈̇ con (Sat b)))
```

A disjunction's condition asks for membership in at least one of the two.

```agda
  cond (a ⇒̇ b) =
    ((var zero ∈̇ con (Sat a)) ⇒̇ (var zero ∈̇ con (Sat b)))
```

An implication's condition says that membership in the antecedent's set implies membership in the consequent's set.

```agda
  cond ⊥̇ = ⊥̇
```

Falsity is its own condition: no environment satisfies it.

```agda
  cond (∃̇ a) =
    (∃̇∈ (con B) (∃̇ ( consAtL zero (suc zero) (suc (suc zero))
                  ∧̇ (var zero ∈̇ con (Sat a)) )))
```

An unbounded existential ranges over the carrier: some member `x` of `B` extends the environment, the extension clause certifies that the new list is an environment, and the extended environment belongs to the subformula's set.

```agda
  cond (∀̇ a) =
    (∀̇∈ (con B) (∀̇ ( consAtL zero (suc zero) (suc (suc zero))
                  ⇒̇ (var zero ∈̇ con (Sat a)) )))
```

The unbounded universal is its dual: every member of the carrier, once consed, lands the extended environment in the subformula's set.

```agda
  cond (∀̇∈ t a) =
    (∀̇ ( tmIs t zero (suc zero)
      ⇒̇ ∀̇∈ (con B) ( (var zero ∈̇ var (suc zero))
                   ⇒̇ ∀̇ ( consAtL zero (suc zero) (suc (suc (suc zero)))
                       ⇒̇ (var zero ∈̇ con (Sat a)) ) ) ))
```

A bounded universal runs in three quantified layers. The outermost reads the value `w` of the bounding term from its slot; over each such `w`, the carrier member `x` is quantified with the two guards `x ∈ B` and `x ∈ w`; and for each `x`, the extension `e'` of the environment by `x`, certified by the extension clause, is required to belong to the subformula's set. Here `w` is only the auxiliary slot of the bound; the environment of the subformula `a` is `e'`, which adds exactly one entry to the environment.

```agda
  cond (∃̇∈ t a) =
    (∃̇ ( tmIs t zero (suc zero)
      ∧̇ ∃̇∈ (con B) ( (var zero ∈̇ var (suc zero))
                   ∧̇ ∃̇ ( consAtL zero (suc zero) (suc (suc (suc zero)))
                       ∧̇ (var zero ∈̇ con (Sat a)) ) ) ))
```

The bounded existential composes the same three layers as an existence statement: the bounding term's value is read first, and the witness is a member of the carrier lying in that value, whose extension belongs to the subformula's set. Both guards, the base and the bound, are kept.

## Reading the conditions

The general equation `Sat-mem` separates membership in the environment set from satisfaction of the condition. Conjunction, disjunction, implication, and falsity reduce directly by the definition of `cond`; no auxiliary equivalence is needed for them. The remaining helpers expose the witnesses hidden by the two atomic existentials and by the existential quantifiers, or read the functions supplied by universal quantifiers. They concern only satisfaction of `cond φ`; the environment-set conjunct remains in `Sat-mem`.

```agda
  CondAtom : ∀ {n} → Term S n → Term S n
           → (S → S → Type (ℓ-suc ℓ)) → S → Type (ℓ-suc ℓ)
  CondAtom t u R z = Σ[ v ∈ S ] (Σ[ w ∈ S ]
    (⟨ (w ∷ v ∷ z ∷ []) ⊨ tmIs t (suc zero) (suc (suc zero)) ⟩
     × (⟨ (w ∷ v ∷ z ∷ []) ⊨ tmIs u zero (suc (suc zero)) ⟩ × R v w)))
```

For the two atoms, the condition is an existence statement, and its unpacked shape is the Σ-type `CondAtom`: a value `v` for `t` and a value `w` for `u`, each read through the term reader against the environment at `z`, together with the relation `R` between the two underlying sets. The type itself carries no truncation; the truncated form appears at the helpers below.

```agda
  cond∈-in : ∀ {n} (t u : Term S n) (z : S)
           → ∥ CondAtom t u (λ v w → ⟨ fst v ∈ fst w ⟩) z ∥₁
           → ⟨ (z ∷ []) ⊨ cond (t ∈̇ u) ⟩
  cond∈-in t u z = PT.map (λ { (v , (w , r)) → v , ∣ w , r ∣₁ })
```

The inward mapping for membership repackages the truncated triple as the nested witnesses the two quantifiers expect. The elimination is legitimate because the goal, an outer truncation, is itself a proposition, not because of any property of the relation inside.

```agda
  cond∈-out : ∀ {n} (t u : Term S n) (z : S)
            → ⟨ (z ∷ []) ⊨ cond (t ∈̇ u) ⟩
            → ∥ CondAtom t u (λ v w → ⟨ fst v ∈ fst w ⟩) z ∥₁
  cond∈-out t u z = PT.rec squash₁
    (λ { (v , hv) → PT.map (λ { (w , r) → v , (w , r) }) hv })
```

The outward mapping flattens the nested witnesses back into the triple, the whole argument remaining inside truncation.

```agda
  cond≐-in : ∀ {n} (t u : Term S n) (z : S)
           → ∥ CondAtom t u (λ v w → fst v ≡ fst w) z ∥₁
           → ⟨ (z ∷ []) ⊨ cond (t ≐ u) ⟩
  cond≐-in t u z = PT.map (λ { (v , (w , r)) → v , ∣ w , r ∣₁ })
```

The equality atom carries the relation `fst v ≡ fst w`, equality of underlying sets, and its inward mapping is word for word the membership one.

```agda
  cond≐-out : ∀ {n} (t u : Term S n) (z : S)
            → ⟨ (z ∷ []) ⊨ cond (t ≐ u) ⟩
            → ∥ CondAtom t u (λ v w → fst v ≡ fst w) z ∥₁
  cond≐-out t u z = PT.rec squash₁
    (λ { (v , hv) → PT.map (λ { (w , r) → v , (w , r) }) hv })
```

Its outward mapping is likewise the membership one with the relation exchanged.

```agda
  CondQuant : ∀ {n} → Formula S (suc n) → S → Type (ℓ-suc ℓ)
  CondQuant a z = Σ[ x ∈ S ] (⟨ fst x ∈ fst B ⟩
    × (Σ[ e' ∈ S ] (⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩
                    × ⟨ fst e' ∈ fst (Sat a) ⟩)))
```

For the unbounded existential, the unpacked condition is the Σ-type `CondQuant`: a member `x` of the base, an entry `e'` certified by the extension clause to be the environment `z` extended by `x`, and membership of `e'` in the subformula's set. Again the type is untruncated, and the truncation is added at the helpers.

```agda
  cond∃-in : ∀ {n} (a : Formula S (suc n)) (z : S)
           → ∥ CondQuant a z ∥₁ → ⟨ (z ∷ []) ⊨ cond (∃̇ a) ⟩
  cond∃-in a z = PT.map (λ { (x , (x∈ , (e' , r))) → x , (x∈ , ∣ e' , r ∣₁) })
```

Inward folds the extension data into the single truncated witness that the existential's own quantifier provides.

```agda
  cond∃-out : ∀ {n} (a : Formula S (suc n)) (z : S)
            → ⟨ (z ∷ []) ⊨ cond (∃̇ a) ⟩ → ∥ CondQuant a z ∥₁
  cond∃-out a z = PT.rec squash₁
    (λ { (x , (x∈ , hv)) → PT.map (λ { (e' , r) → x , (x∈ , (e' , r)) }) hv })
```

Outward unfolds the two nested truncated witnesses in turn; both goals are truncations and therefore propositions, so the unfolding is legitimate.

```agda
  cond∀-in : ∀ {n} (a : Formula S (suc n)) (z : S)
           → ((x e' : S) → ⟨ fst x ∈ fst B ⟩
              → ⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩
```

For every permitted value and its certified extension, the premise supplies membership in the subformula's satisfaction set.

```agda
              → ⟨ fst e' ∈ fst (Sat a) ⟩)
           → ⟨ (z ∷ []) ⊨ cond (∀̇ a) ⟩
  cond∀-in a z k x x∈ e' hc = k x e' x∈ hc
```

For the unbounded universal, the unpacked condition is a function assigning to every base member and its extension the subformula's truth at that extension. Inward and outward are that one function read in the two directions of the quantifier.

```agda
  cond∀-out : ∀ {n} (a : Formula S (suc n)) (z : S)
            → ⟨ (z ∷ []) ⊨ cond (∀̇ a) ⟩
            → ((x e' : S) → ⟨ fst x ∈ fst B ⟩
```

Reading the condition outward retains the value from `B` and the environment obtained by adjoining it.

```agda
               → ⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩
               → ⟨ fst e' ∈ fst (Sat a) ⟩)
  cond∀-out a z h x e' x∈ hc = h x x∈ e' hc
```

No truncation appears, because satisfaction of a universal is verified by supplying its verifier, which is exactly what both directions do.

```agda
  CondBnd : ∀ {n} → Formula S (suc n) → S → S → Type (ℓ-suc ℓ)
  CondBnd a z w = Σ[ x ∈ S ] ((⟨ fst x ∈ fst B ⟩ × ⟨ fst x ∈ fst w ⟩)
    × (Σ[ e' ∈ S ]
        (⟨ (e' ∷ x ∷ w ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩
         × ⟨ fst e' ∈ fst (Sat a) ⟩)))
```

The bounded quantifiers add one layer. The condition quantifies, in order, the value `w` of the bounding term, a member `x` of the base lying in `w`, and the extension `e'` of the environment `z` by `x`, certified by the extension clause and required to belong to the subformula's set. The role of `w` is auxiliary: it carries the bound's value, while the environment of the subformula is `e'`, which adds exactly one entry, the member `x`, to the environment `z`.

```agda
  cond∃∈-in : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S)
            → ∥ (Σ[ w ∈ S ] (⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩
                             × ∥ CondBnd a z w ∥₁)) ∥₁
            → ⟨ (z ∷ []) ⊨ cond (∃̇∈ t a) ⟩
```

The bounded existential stacks its witnesses: the outer truncation is over the value `w` of the bounding term, and inside it sits the inner truncation of `CondBnd a z w`, holding the carrier member and its extension.

```agda
  cond∃∈-in t a z = PT.map
    (λ { (w , (hw , hx)) → w , (hw , PT.map
      (λ { (x , ((x∈B , x∈w) , (e' , r))) → x , (x∈B , (x∈w , ∣ e' , r ∣₁)) })
      hx) })
```

The first `PT.map` eliminates the outer truncation over `w`, and the nested `PT.map` eliminates the inner truncation of `CondBnd`, folding the member and the extension into the existential's own quantifier. Both goals are truncations and hence propositions, so the two eliminations are legitimate for the same reason.

```agda
  cond∃∈-out : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S)
             → ⟨ (z ∷ []) ⊨ cond (∃̇∈ t a) ⟩
             → ∥ (Σ[ w ∈ S ] (⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩
                              × ∥ CondBnd a z w ∥₁)) ∥₁
```

The outward statement exposes the same two-layer shape: the value of the bound on the outside, and within it the truncated record of the carrier member and its extension.

```agda
  cond∃∈-out t a z = PT.map
    (λ { (w , (hw , hx)) → w , (hw , PT.rec squash₁
      (λ { (x , (x∈B , (x∈w , hv))) → PT.map
        (λ { (e' , r) → x , ((x∈B , x∈w) , (e' , r)) }) hv })
      hx) })
```

Its proof unfolds the two layers in turn, the whole journey remaining inside truncation.

```agda
  cond∀∈-in : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S)
            → ((w : S) → ⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩
               → (x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ fst x ∈ fst w ⟩
```

The two guards require `x` to belong both to the base `B` and to the value `w` of the bounding term.

```agda
               → ⟨ (e' ∷ x ∷ w ∷ z ∷ [])
                    ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩
               → ⟨ fst e' ∈ fst (Sat a) ⟩)
            → ⟨ (z ∷ []) ⊨ cond (∀̇∈ t a) ⟩
  cond∀∈-in t a z k w hw x x∈B x∈w e' hc = k w hw x e' x∈B x∈w hc
```

The bounded universal's condition is a function over the three quantified layers: to every value `w` of the bounding term it assigns, for every base member `x` inside `w` and every extension `e'` certified as the environment `z` extended by `x`, the subformula's truth at `e'`. The inward mapping is that function, applied.

```agda
  cond∀∈-out : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S)
             → ⟨ (z ∷ []) ⊨ cond (∀̇∈ t a) ⟩
             → ((w : S) → ⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩
```

The result ranges over the same bound value, base member, and certified one-entry extension.

```agda
                → (x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ fst x ∈ fst w ⟩
                → ⟨ (e' ∷ x ∷ w ∷ z ∷ [])
                     ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩
                → ⟨ fst e' ∈ fst (Sat a) ⟩)
  cond∀∈-out t a z h w hw x e' x∈B x∈w hc = h w hw x x∈B x∈w e' hc
```

The outward mapping is the same function, read back through the three quantifiers. No truncation appears in either direction, since a universal is verified by supplying its verifier, and here the verifier is supplied layer by layer, for the value, for the member, and for the extension.