AEAD.mk.{u_1, u_2, u_3, u_4}
  {KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {PTType 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)`. } {ADType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  (encryptK → PT → AD → CT : KType u_1 → PTType u_2 → ADType u_4 → CTType u_3)
  (decryptK → CT → AD → Option PT : KType u_1 → CTType u_3 → ADType u_4 → OptionOption.{u} (α : Type u) : Type uOptional values, which are either `some` around a value from the underlying type or `none`.

`Option` can represent nullable types or computations that might fail. In the codomain of a function
type, it can also represent partiality.
 PTType u_2)
  (correctness∀ (k : K) (pt : PT) (ad : AD), decrypt k (encrypt k pt ad) ad = some pt :
    ∀ (kK : KType u_1) (ptPT : PTType u_2) (adAD : ADType u_4),
      decryptK → CT → AD → Option PT kK (encryptK → PT → AD → CT kK ptPT adAD) adAD =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`.
        someOption.some.{u} {α : Type u} (val : α) : Option αSome value of type `α`.  ptPT) :
  AEADAEAD.{u_1, u_2, u_3, u_4} (K : Type u_1) (PT : Type u_2) (CT : Type u_3) (AD : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)AEAD scheme parameterized by key `K`, plaintext `PT`, ciphertext `CT`,
and associated data `AD`. The `correctness` field guarantees that decrypting
an honestly encrypted ciphertext with the correct key and AD recovers the
original plaintext.  KType u_1 PTType u_2 CTType u_3 ADType u_4