theorem PQXDH_agree.{u_1, u_2, u_3, u_4, u_5, u_6,
    u_7, u_8}
  {FType u_8 : Type u_8A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  FType u_8] {GType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_6] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  FType u_8 GType u_6]
  {SKType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {PK_kemType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {SK_kemType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {CTType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {SSType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {S_sigType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  (kemKEM PK_kem SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PK_kemType u_1 SK_kemType u_2 CTType u_3 SSType u_4)
  (kdfKDF ((G × G × G × G) × SS) SK : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_6 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_6 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_6 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_6)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SKType u_7)
  (G₀G : GType u_6) (ikₐF ekₐF ikᵦF spkᵦF opkᵦF : FType u_8)
  (sk_kemSK_kem : SK_kemType u_2) (pk_kemPK_kem : PK_kemType u_1)
  (s1S_sig s2S_sig : S_sigType u_5)
  {IKₐG EKₐG IKᵦG SPKᵦG OPKᵦG : GType u_6}
  (hIKₐIKₐ = DH ikₐ G₀ : IKₐG =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. DHDH.{u_1, u_2} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G] (a : F) (B : G) : GDiffie-Hellman function: DH(a, B) = a • B.  ikₐF G₀G)
  (hEKₐEKₐ = DH ekₐ G₀ : EKₐG =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. DHDH.{u_1, u_2} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G] (a : F) (B : G) : GDiffie-Hellman function: DH(a, B) = a • B.  ekₐF G₀G)
  (hIKᵦIKᵦ = DH ikᵦ G₀ : IKᵦG =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. DHDH.{u_1, u_2} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G] (a : F) (B : G) : GDiffie-Hellman function: DH(a, B) = a • B.  ikᵦF G₀G)
  (hSPKᵦSPKᵦ = DH spkᵦ G₀ : SPKᵦG =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. DHDH.{u_1, u_2} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G] (a : F) (B : G) : GDiffie-Hellman function: DH(a, B) = a • B.  spkᵦF G₀G)
  (hOPKᵦOPKᵦ = DH opkᵦ G₀ : OPKᵦG =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. DHDH.{u_1, u_2} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G] (a : F) (B : G) : GDiffie-Hellman function: DH(a, B) = a • B.  opkᵦF G₀G)
  (bundlePQXDHBundle G PK_kem S_sig : PQXDHBundlePQXDHBundle.{u_1, u_2, u_3} (G : Type u_1) (PK_kem : Type u_2) (S_sig : Type u_3) [AddCommGroup G] :
  Type (max (max u_1 u_2) u_3)§2.3, p. 472 and Figure 1, p. 471: Bob's prekey bundle including the
post-quantum KEM public key and signatures authenticating the signed prekeys.
"In the initial message to Alex, Blake includes PQSPKᵦᵖᵏ and
sign(PQSPKᵦᵖᵏ, IKᵦˢᵏ)." (§2.3, item 2, p. 472)  GType u_6 PK_kemType u_1 S_sigType u_5)
  (hBundlebundle = { IKᵦ := IKᵦ, SPKᵦ := SPKᵦ, sig_spk := s1, OPKᵦ := OPKᵦ, PQSPK := pk_kem, sig_pqspk := s2 } :
    bundlePQXDHBundle G PK_kem S_sig =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      {PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig IKᵦG :=PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig IKᵦG,PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig SPKᵦG :=PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig SPKᵦG,PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig
        sig_spkS_sig :=PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig s1S_sig,PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig OPKᵦG :=PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig OPKᵦG,PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig
        PQSPKPK_kem :=PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig pk_kemPK_kem,PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig
        sig_pqspkS_sig :=PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig s2S_sig }PQXDHBundle.mk.{u_1, u_2, u_3} {G : Type u_1} {PK_kem : Type u_2} {S_sig : Type u_3} [AddCommGroup G] (IKᵦ SPKᵦ : G)
  (sig_spk : S_sig) (OPKᵦ : G) (PQSPK : PK_kem) (sig_pqspk : S_sig) : PQXDHBundle G PK_kem S_sig)
  (ctCT : CTType u_3) (ssSS : SSType u_4)
  (hEncapskem.encaps pk_kem = (ct, ss) : kemKEM PK_kem SK_kem CT SS.encapsKEM.encaps.{u_1, u_2, u_3, u_4} {PK : Type u_1} {SK_kem : Type u_2} {CT : Type u_3} {SS : Type u_4}
  (self : KEM PK SK_kem CT SS) : PK → CT × SS pk_kemPK_kem =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. (Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.ctCT,Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. ssSS)Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.)
  (hDecapskem.decaps sk_kem ct = ss : kemKEM PK_kem SK_kem CT SS.decapsKEM.decaps.{u_1, u_2, u_3, u_4} {PK : Type u_1} {SK_kem : Type u_2} {CT : Type u_3} {SS : Type u_4}
  (self : KEM PK SK_kem CT SS) : SK_kem → CT → SS sk_kemSK_kem ctCT =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ssSS) :
  PQXDH_SK_AlicePQXDH_SK_Alice.{u_1, u_2, u_3, u_4, u_5, u_6, u_7, u_8} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G]
  [Module F G] {SK : Type u_3} {PK_kem : Type u_4} {SK_kem : Type u_5} {CT : Type u_6} {SS : Type u_7}
  {S_sig : Type u_8} (kem : KEM PK_kem SK_kem CT SS) (kdf : KDF ((G × G × G × G) × SS) SK) (ikₐ ekₐ : F)
  (bundle : PQXDHBundle G PK_kem S_sig) : SKFigure 1, p. 471: Alice derives the PQXDH session key
SK_B = kdf(ikₐ • SPKᵦ ‖ ekₐ • IKᵦ ‖ ekₐ • SPKᵦ ‖ SS).  kemKEM PK_kem SK_kem CT SS kdfKDF ((G × G × G × G) × SS) SK ikₐF ekₐF bundlePQXDHBundle G PK_kem S_sig =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    PQXDH_SK_BobPQXDH_SK_Bob.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G]
  {SK : Type u_3} {PK_kem : Type u_4} {SK_kem : Type u_5} {CT : Type u_6} {SS : Type u_7}
  (kem : KEM PK_kem SK_kem CT SS) (kdf : KDF ((G × G × G × G) × SS) SK) (ikᵦ spkᵦ opkᵦ : F) (sk_kem : SK_kem)
  (IKₐ EKₐ : G) (ct : CT) : SKFigure 1, p. 471: Bob derives the PQXDH session key
SKₐ = kdf(spkᵦ • IKₐ ‖ ikᵦ • EKₐ ‖ spkᵦ • EKₐ ‖ SS).  kemKEM PK_kem SK_kem CT SS kdfKDF ((G × G × G × G) × SS) SK ikᵦF spkᵦF opkᵦF
      sk_kemSK_kem IKₐG EKₐG ctCT