proofs.rs

Recorded run

Toolchain source metadata: not recorded.

Run locally

git clone -- https://github.com/MasWag/crate-proofs report-16-source-1
git -C report-16-source-1 checkout --detach d515d59559746c5bbca74d3e33626cc814519a48
git -C report-16-source-1 submodule update --init --recursive --checkout
cd report-16-source-1/option-ext/0.2.0/.work/build/default/aarch64-apple-darwin/proofs

lake build +AdaptedContracts +Contracts

printf '%s' 'import Aeneas
import AdaptedContracts
import Contracts
set_option pp.all true
set_option pp.universes true
set_option pp.explicit true
set_option pp.fullNames true
set_option pp.notation false
set_option pp.proofs true
set_option pp.deepTerms true
set_option pp.maxSteps 10000000
-- proofs.rs adapter for Lean 4.35.0 / Aeneas be86ab0f.
-- Uses Lean'\''s environment, Meta telescope and pretty-printer, never source parsing.
open Lean Meta Elab Command
namespace ProofsProbe
meta def moduleOf (env : Environment) (n : Name) : String :=
  match env.getModuleIdxFor? n with
  | some idx => env.header.moduleNames[idx.toNat]!.toString
  | none => ""
meta def pretty (e : Expr) : MetaM String := do
  let s := (← ppExpr e).pretty
  if s.contains '\''⋯'\'' then
    throwError "Lean display contains an omission marker (or literal ⋯); refusing an incomplete proposition"
  if s.utf8ByteSize > 1000000 then throwError "Proposition exceeds 1,000,000-byte recording limit"
  return s
-- The full statement stays explicit; the inspection view uses Lean notation.
meta def readable (e : Expr) : MetaM String :=
  withOptions (fun o =>
    let o := o.setBool `pp.all false
    let o := o.setBool `pp.explicit false
    let o := o.setBool `pp.universes false
    o.setBool `pp.notation true) (pretty e)
-- Only a constant'\''s own tag grants a link; names in plain text are never guessed.
partial def segments (code : Widget.CodeWithInfos) (ref : Option Name := none) : Array Json :=
  match code with
  | .text text => #[Json.mkObj (([("text", toJson text)]) ++
      (ref.toList.map fun n => ("ref", toJson n.toString)))]
  | .append parts => parts.foldl (fun acc part => acc ++ segments part ref) #[]
  | .tag info part =>
    let ref := match info.info.val.info with
      | .ofTermInfo ti => ti.expr.constName?
      | _ => none
    segments part ref
meta def readableFields (key : String) (e : Expr) : MetaM (List (String × Json)) := do
  let text ← readable e
  let base := [(key, toJson text)]
  try
    let code ← withOptions (fun o =>
      let o := o.setBool `pp.all false
      let o := o.setBool `pp.explicit false
      let o := o.setBool `pp.universes false
      let o := o.setBool `pp.notation true
      o.setBool `pp.tagAppFns true) (Widget.ppExprTagged e)
    let parts := segments code
    let joined := String.join (parts.toList.map fun j =>
      (j.getObjValAs? String "text").toOption.getD "")
    if joined != text || parts.size > 10000 || joined.utf8ByteSize > 1000000 then
      return base
    return base ++ [(key ++ "_segments", toJson parts)]
  catch _ => return base
meta def inspect (n : Name) (ty : Expr) (manual : Bool) : MetaM (Option Json) := do
  let env ← getEnv
  forallTelescope ty fun xs conclusion => do
    let programExpr ← try
      let normalized ← Aeneas.Utils.normalizeLetBindings conclusion
      let (expr, _) ← Aeneas.Step.getStepSpecFunArgsExpr normalized
      pure (some expr)
    catch _ => pure none
    if programExpr.isNone && !manual then return none
    let full ← pretty ty
    let program ← match programExpr with
      | some expr => pure (toJson (← readable expr))
      | none => pure Json.null
    let head := toJson (programExpr.bind (·.getAppFn.constName?) |>.map Name.toString)
    let mut binders := #[]
    for x in xs do
      let d ← x.fvarId!.getDecl
      let prop ← isProp d.type
      binders := binders.push (Json.mkObj ((← readableFields "type" d.type) ++ [
        ("name", toJson d.userName.toString),
        ("kind", toJson (if d.binderInfo.isInstImplicit then "instance" else if prop then "hypothesis" else "variable")),
        ("binder", toJson (if d.binderInfo.isInstImplicit then "instance" else if d.binderInfo.isExplicit then "explicit" else "implicit"))]))
    if binders.size > 1000 then throwError "More than 1000 binders"
    let some ranges ← findDeclarationRanges? n | throwError "Missing theorem source range: {n}"
    let axioms ← Lean.collectAxioms n
    let constants := ty.getUsedConstants
    let mut definitions := #[]
    for nm in constants.extract 0 100 do
      let ranges ← findDeclarationRanges? nm
      definitions := definitions.push (Json.mkObj [
        ("name", toJson nm.toString), ("module", toJson (moduleOf env nm)),
        ("source", match ranges with
          | some r => Json.mkObj [("first_line", toJson r.range.pos.line), ("last_line", toJson r.range.endPos.line)]
          | none => Json.null)])
    return some (Json.mkObj ((← readableFields "conclusion" conclusion) ++ [
      ("version", toJson (1 : Nat)), ("theorem", toJson n.toString),
      ("module", toJson (moduleOf env n)), ("statement", toJson full),
      ("binders", toJson binders),
      ("program", program), ("program_head", head),
      ("axioms", toJson (axioms.map Name.toString)),
      ("first_line", toJson ranges.range.pos.line), ("last_line", toJson ranges.range.endPos.line),
      ("definitions", toJson definitions), ("definitions_truncated", toJson (decide (constants.size > 100))),
      ("translation_rerun", toJson false)]))
end ProofsProbe

run_cmd do
  let manual : Array Name := #[`OptionExtContracts.contains_relation_correct, `OptionExtContracts.map_or2_correct, `OptionExtAdaptedContracts.map_or_else2_correct]
  let localModules : Array String := #[]
  let roots : Array Name := #[]
  let env ← getEnv
  let mut closure : Array Name := #[]
  let mut pending := roots.toList
  while !pending.isEmpty do
    let m := pending.head!
    pending := pending.tail!
    if !closure.contains m then
      closure := closure.push m
      if let some idx := env.header.moduleNames.findIdx? (· == m) then
        pending := (env.header.moduleData[idx]!.imports.toList.map (·.module)) ++ pending
  let scope := closure.filter (fun m => localModules.contains m.toString)
  for n in manual do
    match env.find? n with
    | some (.thmInfo _) => pure ()
    | _ => throwError "Expected a theorem: {n}"
  for (n, ci) in env.constants.toList do
    let explicit := manual.contains n
    if explicit || scope.contains (ProofsProbe.moduleOf env n).toName then
      if let .thmInfo th := ci then
        let result ← liftTermElabM <| ProofsProbe.inspect n th.type explicit
        if let some value := result then
          liftIO <| IO.println ("proofs.rs:formal:" ++ value.compress)

run_cmd do
  let theorem_name := `OptionExtContracts.contains_relation_correct
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: OptionExtContracts.contains_relation_correct"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in OptionExtContracts.contains_relation_correct: {ax}"
  liftIO <| IO.println "proofs.rs:checked:OptionExtContracts.contains_relation_correct"

run_cmd do
  let theorem_name := `OptionExtContracts.map_or2_correct
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: OptionExtContracts.map_or2_correct"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in OptionExtContracts.map_or2_correct: {ax}"
  liftIO <| IO.println "proofs.rs:checked:OptionExtContracts.map_or2_correct"

run_cmd do
  let theorem_name := `OptionExtAdaptedContracts.map_or_else2_correct
  match (← getEnv).find? theorem_name with
  | some (.thmInfo _) => pure ()
  | _ => throwError "Expected a theorem: OptionExtAdaptedContracts.map_or_else2_correct"
  let axioms ← Lean.collectAxioms theorem_name
  for ax in axioms do
    unless [``propext, ``Classical.choice, ``Quot.sound].contains ax do
      throwError "Unapproved axiom in OptionExtAdaptedContracts.map_or_else2_correct: {ax}"
  liftIO <| IO.println "proofs.rs:checked:OptionExtAdaptedContracts.map_or_else2_correct"
' | lake env lean --stdin

Checks out the recorded source commit from GitHub. Install the report’s tool version before running.

Source on GitHub · SARIF with logs (.json)

Recorded run

Completed · 3 checks passed · 0 failed

2026-11-03T13:03:16.830847+00:00 · 21.3 seconds · Exit code 0

Recorded on the author’s machine.

CheckResultClaim
Lean checked theorem OptionExtContracts.contains_relation_correct; axioms limited to propext, Classical.choice, Quot.sound
OptionExtContracts.contains_relation_correct
PassedClaim #1
Lean checked theorem OptionExtContracts.map_or2_correct; axioms limited to propext, Classical.choice, Quot.sound
OptionExtContracts.map_or2_correct
PassedClaim #2
Lean checked theorem OptionExtAdaptedContracts.map_or_else2_correct; axioms limited to propext, Classical.choice, Quot.sound
OptionExtAdaptedContracts.map_or_else2_correct
PassedClaim #3
Execution details
Started
2026-11-03T13:03:16.830847+00:00
Finished
2026-11-03T13:03:38.107883+00:00
Platform
macos aarch64
Rust compiler
rustc 1.94.1 (e408947bf 2026-03-25) binary: rustc commit-hash: e408947bfd200af42db322daf0fadfe7e26d3bd1 commit-date: 2026-03-25 host: aarch64-apple-darwin release: 1.94.1 LLVM version: 21.1.8
Working directory
option-ext/0.2.0/.work/build/default/aarch64-apple-darwin/proofs
Environment overrides
None recorded
Git repository
https://github.com/MasWag/crate-proofs
Git commit
d515d59559746c5bbca74d3e33626cc814519a48
Diagnostics & logs
=== stdout ===
✔ [1796/1799] Built OptionExtAdapted (1.5s)
✔ [1797/1799] Built OptionExt (1.5s)
✔ [1798/1799] Built AdaptedContracts (1.7s)
✔ [1799/1799] Built Contracts (1.7s)
Build completed successfully (1799 jobs).

$ lake env lean --stdin (proofs.rs formal extraction and axiom audit)
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"T","type":"Type","type_segments":[{"text":"Type"}]},{"binder":"implicit","kind":"variable","name":"U","type":"Type","type_segments":[{"text":"Type"}]},{"binder":"implicit","kind":"variable","name":"F","type":"Type","type_segments":[{"text":"Type"}]},{"binder":"implicit","kind":"variable","name":"D","type":"Type","type_segments":[{"text":"Type"}]},{"binder":"explicit","kind":"variable","name":"fInst","type":"Aeneas.Std.core.ops.function.FnOnce F T U","type_segments":[{"ref":"Aeneas.Std.core.ops.function.FnOnce","text":"Aeneas.Std.core.ops.function.FnOnce"},{"text":" "},{"text":"F"},{"text":" "},{"text":"T"},{"text":" "},{"text":"U"}]},{"binder":"explicit","kind":"variable","name":"dInst","type":"Aeneas.Std.core.ops.function.FnOnce D Unit U","type_segments":[{"ref":"Aeneas.Std.core.ops.function.FnOnce","text":"Aeneas.Std.core.ops.function.FnOnce"},{"text":" "},{"text":"D"},{"text":" "},{"ref":"Unit","text":"Unit"},{"text":" "},{"text":"U"}]},{"binder":"explicit","kind":"variable","name":"self","type":"Option T","type_segments":[{"ref":"Option","text":"Option"},{"text":" "},{"text":"T"}]},{"binder":"explicit","kind":"variable","name":"f","type":"F","type_segments":[{"text":"F"}]},{"binder":"explicit","kind":"variable","name":"d","type":"D","type_segments":[{"text":"D"}]},{"binder":"explicit","kind":"variable","name":"mapping","type":"T → U","type_segments":[{"text":"T"},{"text":" → "},{"text":"U"}]},{"binder":"explicit","kind":"variable","name":"defaultValue","type":"U","type_segments":[{"text":"U"}]},{"binder":"explicit","kind":"hypothesis","name":"selected","type":"match self with\n| Option.none => dInst.call_once d () = Aeneas.Std.Result.ok defaultValue\n| Option.some x => fInst.call_once f x = Aeneas.Std.Result.ok (mapping x)","type_segments":[{"text":"match "},{"text":"self"},{"text":" with\n| "},{"ref":"Option.none","text":"Option.none"},{"text":" => "},{"text":"dInst"},{"text":"."},{"ref":"Aeneas.Std.core.ops.function.FnOnce.call_once","text":"call_once"},{"text":" "},{"text":"d"},{"text":" "},{"ref":"Unit.unit","text":"("},{"ref":"Unit.unit","text":")"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"defaultValue"},{"text":"\n| "},{"ref":"Option.some","text":"Option.some"},{"text":" "},{"text":"x"},{"text":" => "},{"text":"fInst"},{"text":"."},{"ref":"Aeneas.Std.core.ops.function.FnOnce.call_once","text":"call_once"},{"text":" "},{"text":"f"},{"text":" "},{"text":"x"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"("},{"text":"mapping"},{"text":" "},{"text":"x"},{"text":")"}]}],"conclusion":"∃ u,\n  OptionExtAdaptedContracts.mapOrElse fInst dInst self f d = Aeneas.Std.Result.ok u ∧\n    u = OptionExtAdaptedContracts.mapLazyDefault mapping defaultValue self","conclusion_segments":[{"text":"∃ "},{"text":"u"},{"text":",\n  "},{"ref":"OptionExtAdaptedContracts.mapOrElse","text":"OptionExtAdaptedContracts.mapOrElse"},{"text":" "},{"text":"fInst"},{"text":" "},{"text":"dInst"},{"text":" "},{"text":"self"},{"text":" "},{"text":"f"},{"text":" "},{"text":"d"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"u"},{"ref":"And","text":" ∧\n    "},{"text":"u"},{"ref":"Eq","text":" = "},{"ref":"OptionExtAdaptedContracts.mapLazyDefault","text":"OptionExtAdaptedContracts.mapLazyDefault"},{"text":" "},{"text":"mapping"},{"text":" "},{"text":"defaultValue"},{"text":" "},{"text":"self"}],"definitions":[{"module":"Aeneas.Std.Core.Ops","name":"Aeneas.Std.core.ops.function.FnOnce","source":{"first_line":44,"last_line":46}},{"module":"Init.Prelude","name":"Unit","source":{"first_line":214,"last_line":224}},{"module":"Init.Prelude","name":"Option","source":{"first_line":3047,"last_line":3058}},{"module":"AdaptedContracts","name":"OptionExtAdaptedContracts.mapLazyDefault.match_1","source":null},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Aeneas.Std.Core.Ops","name":"Aeneas.Std.core.ops.function.FnOnce.call_once","source":{"first_line":46,"last_line":46}},{"module":"Init.Prelude","name":"Unit.unit","source":{"first_line":226,"last_line":231}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"AdaptedContracts","name":"OptionExtAdaptedContracts.mapOrElse","source":{"first_line":6,"last_line":6}},{"module":"AdaptedContracts","name":"OptionExtAdaptedContracts.mapLazyDefault","source":{"first_line":8,"last_line":13}}],"definitions_truncated":false,"first_line":38,"last_line":50,"module":"AdaptedContracts","program":null,"program_head":null,"statement":"∀ {T U F D : Type} (fInst : Aeneas.Std.core.ops.function.FnOnce.{0, 0, 0} F T U)\n  (dInst : Aeneas.Std.core.ops.function.FnOnce.{0, 0, 0} D Unit U) (self : Option.{0} T) (f : F) (d : D)\n  (mapping : T → U) (defaultValue : U)\n  (selected :\n    @OptionExtAdaptedContracts.mapLazyDefault.match_1.{1} T (fun (self : Option.{0} T) => Prop) self\n      (fun (_ : Unit) =>\n        @Eq.{1} (Aeneas.Std.Result.{0} U)\n          (@Aeneas.Std.core.ops.function.FnOnce.call_once.{0, 0, 0} D Unit U dInst d Unit.unit)\n          (@Aeneas.Std.Result.ok.{0} U defaultValue))\n      fun (x : T) =>\n      @Eq.{1} (Aeneas.Std.Result.{0} U) (@Aeneas.Std.core.ops.function.FnOnce.call_once.{0, 0, 0} F T U fInst f x)\n        (@Aeneas.Std.Result.ok.{0} U (mapping x))),\n  @Exists.{1} U fun (u : U) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} U)\n        (@OptionExtAdaptedContracts.mapOrElse.{0, 0, 0, 0} T U F D fInst dInst self f d)\n        (@Aeneas.Std.Result.ok.{0} U u))\n      (@Eq.{1} U u (@OptionExtAdaptedContracts.mapLazyDefault T U mapping defaultValue self))","theorem":"OptionExtAdaptedContracts.map_or_else2_correct","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"T","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"implicit","kind":"variable","name":"U","type":"Type u_2","type_segments":[{"text":"Type u_2"}]},{"binder":"explicit","kind":"variable","name":"eqInst","type":"Aeneas.Std.core.cmp.PartialEq U T","type_segments":[{"ref":"Aeneas.Std.core.cmp.PartialEq","text":"Aeneas.Std.core.cmp.PartialEq"},{"text":" "},{"text":"U"},{"text":" "},{"text":"T"}]},{"binder":"explicit","kind":"variable","name":"relation","type":"U → T → Prop","type_segments":[{"text":"U"},{"text":" → "},{"text":"T"},{"text":" → "},{"text":"Prop"}]},{"binder":"explicit","kind":"variable","name":"opt","type":"Option T","type_segments":[{"ref":"Option","text":"Option"},{"text":" "},{"text":"T"}]},{"binder":"explicit","kind":"variable","name":"x","type":"U","type_segments":[{"text":"U"}]},{"binder":"explicit","kind":"hypothesis","name":"selected","type":"∀ (t : T), opt = Option.some t → ∃ b, eqInst.eq x t = Aeneas.Std.Result.ok b ∧ (b = Bool.true ↔ relation x t)","type_segments":[{"text":"∀ ("},{"text":"t"},{"text":" : "},{"text":"T"},{"text":"), "},{"text":"opt"},{"ref":"Eq","text":" = "},{"ref":"Option.some","text":"Option.some"},{"text":" "},{"text":"t"},{"text":" → "},{"text":"∃ "},{"text":"b"},{"text":", "},{"text":"eqInst"},{"text":"."},{"ref":"Aeneas.Std.core.cmp.PartialEq.eq","text":"eq"},{"text":" "},{"text":"x"},{"text":" "},{"text":"t"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"b"},{"ref":"And","text":" ∧ "},{"ref":"Iff","text":"("},{"text":"b"},{"ref":"Eq","text":" = "},{"ref":"Bool.true","text":"Bool.true"},{"ref":"Iff","text":" ↔ "},{"text":"relation"},{"text":" "},{"text":"x"},{"text":" "},{"text":"t"},{"ref":"Iff","text":")"}]}],"conclusion":"∃ out,\n  OptionExtContracts.contains eqInst opt x = Aeneas.Std.Result.ok out ∧\n    (out = Bool.true ↔\n      match opt, selected with\n      | Option.none, selected => False\n      | Option.some t, selected => relation x t)","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"ref":"OptionExtContracts.contains","text":"OptionExtContracts.contains"},{"text":" "},{"text":"eqInst"},{"text":" "},{"text":"opt"},{"text":" "},{"text":"x"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧\n    "},{"ref":"Iff","text":"("},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"Bool.true","text":"Bool.true"},{"ref":"Iff","text":" ↔\n      "},{"text":"match "},{"text":"opt"},{"text":", "},{"text":"selected"},{"text":" with\n      | "},{"ref":"Option.none","text":"Option.none"},{"text":", "},{"text":"selected"},{"text":" => "},{"ref":"False","text":"False"},{"text":"\n      | "},{"ref":"Option.some","text":"Option.some"},{"text":" "},{"text":"t"},{"text":", "},{"text":"selected"},{"text":" => "},{"text":"relation"},{"text":" "},{"text":"x"},{"text":" "},{"text":"t"},{"ref":"Iff","text":")"}],"definitions":[{"module":"Aeneas.Std.Core.Cmp","name":"Aeneas.Std.core.cmp.PartialEq","source":{"first_line":13,"last_line":16}},{"module":"Init.Prelude","name":"Option","source":{"first_line":3047,"last_line":3058}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Init.Prelude","name":"Option.some","source":{"first_line":3057,"last_line":3058}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"Bool","source":{"first_line":99,"last_line":111}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Aeneas.Std.Core.Cmp","name":"Aeneas.Std.core.cmp.PartialEq.eq","source":{"first_line":15,"last_line":15}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Core","name":"Iff","source":{"first_line":183,"last_line":194}},{"module":"Init.Prelude","name":"Bool.true","source":{"first_line":110,"last_line":111}},{"module":"Contracts","name":"OptionExtContracts.contains","source":{"first_line":19,"last_line":19}},{"module":"Contracts","name":"OptionExtContracts.contains_relation_correct.match_1","source":null},{"module":"Init.Prelude","name":"Option.none","source":{"first_line":3055,"last_line":3056}},{"module":"Init.Prelude","name":"False","source":{"first_line":274,"last_line":282}}],"definitions_truncated":false,"first_line":38,"last_line":49,"module":"Contracts","program":null,"program_head":null,"statement":"∀ {T : Type u_1} {U : Type u_2} (eqInst : Aeneas.Std.core.cmp.PartialEq.{u_2, u_1} U T) (relation : U → T → Prop)\n  (opt : Option.{u_1} T) (x : U)\n  (selected :\n    ∀ (t : T),\n      @Eq.{u_1 + 1} (Option.{u_1} T) opt (@Option.some.{u_1} T t) →\n        @Exists.{1} Bool fun (b : Bool) =>\n          And\n            (@Eq.{1} (Aeneas.Std.Result.{0} Bool) (@Aeneas.Std.core.cmp.PartialEq.eq.{u_2, u_1} U T eqInst x t)\n              (@Aeneas.Std.Result.ok.{0} Bool b))\n            (Iff (@Eq.{1} Bool b Bool.true) (relation x t))),\n  @Exists.{1} Bool fun (out : Bool) =>\n    And\n      (@Eq.{1} (Aeneas.Std.Result.{0} Bool) (@OptionExtContracts.contains.{u_1, u_2} T U eqInst opt x)\n        (@Aeneas.Std.Result.ok.{0} Bool out))\n      (Iff (@Eq.{1} Bool out Bool.true)\n        (@OptionExtContracts.contains_relation_correct.match_1.{u_1, u_2, 1} T U eqInst relation x\n          (fun (opt : Option.{u_1} T)\n              (selected :\n                ∀ (t : T),\n                  @Eq.{u_1 + 1} (Option.{u_1} T) opt (@Option.some.{u_1} T t) →\n                    @Exists.{1} Bool fun (b : Bool) =>\n                      And\n                        (@Eq.{1} (Aeneas.Std.Result.{0} Bool)\n                          (@Aeneas.Std.core.cmp.PartialEq.eq.{u_2, u_1} U T eqInst x t)\n                          (@Aeneas.Std.Result.ok.{0} Bool b))\n                        (Iff (@Eq.{1} Bool b Bool.true) (relation x t))) =>\n            Prop)\n          opt selected\n          (fun\n              (selected :\n                ∀ (t : T),\n                  @Eq.{u_1 + 1} (Option.{u_1} T) (@Option.none.{u_1} T) (@Option.some.{u_1} T t) →\n                    @Exists.{1} Bool fun (b : Bool) =>\n                      And\n                        (@Eq.{1} (Aeneas.Std.Result.{0} Bool)\n                          (@Aeneas.Std.core.cmp.PartialEq.eq.{u_2, u_1} U T eqInst x t)\n                          (@Aeneas.Std.Result.ok.{0} Bool b))\n                        (Iff (@Eq.{1} Bool b Bool.true) (relation x t))) =>\n            False)\n          fun (t : T)\n            (selected :\n              ∀ (t_1 : T),\n                @Eq.{u_1 + 1} (Option.{u_1} T) (@Option.some.{u_1} T t) (@Option.some.{u_1} T t_1) →\n                  @Exists.{1} Bool fun (b : Bool) =>\n                    And\n                      (@Eq.{1} (Aeneas.Std.Result.{0} Bool)\n                        (@Aeneas.Std.core.cmp.PartialEq.eq.{u_2, u_1} U T eqInst x t_1)\n                        (@Aeneas.Std.Result.ok.{0} Bool b))\n                      (Iff (@Eq.{1} Bool b Bool.true) (relation x t_1))) =>\n          relation x t))","theorem":"OptionExtContracts.contains_relation_correct","translation_rerun":false,"version":1}
proofs.rs:formal:{"axioms":["propext","Quot.sound"],"binders":[{"binder":"implicit","kind":"variable","name":"T","type":"Type u_1","type_segments":[{"text":"Type u_1"}]},{"binder":"implicit","kind":"variable","name":"V","type":"Type u_2","type_segments":[{"text":"Type u_2"}]},{"binder":"implicit","kind":"variable","name":"F","type":"Type u_3","type_segments":[{"text":"Type u_3"}]},{"binder":"explicit","kind":"variable","name":"call","type":"Aeneas.Std.core.ops.function.FnOnce F T V","type_segments":[{"ref":"Aeneas.Std.core.ops.function.FnOnce","text":"Aeneas.Std.core.ops.function.FnOnce"},{"text":" "},{"text":"F"},{"text":" "},{"text":"T"},{"text":" "},{"text":"V"}]},{"binder":"explicit","kind":"variable","name":"mapping","type":"T → V","type_segments":[{"text":"T"},{"text":" → "},{"text":"V"}]},{"binder":"explicit","kind":"variable","name":"opt","type":"Option T","type_segments":[{"ref":"Option","text":"Option"},{"text":" "},{"text":"T"}]},{"binder":"explicit","kind":"variable","name":"f","type":"F","type_segments":[{"text":"F"}]},{"binder":"explicit","kind":"variable","name":"default","type":"V","type_segments":[{"text":"V"}]},{"binder":"explicit","kind":"hypothesis","name":"selected","type":"∀ (t : T), opt = Option.some t → call.call_once f t = Aeneas.Std.Result.ok (mapping t)","type_segments":[{"text":"∀ ("},{"text":"t"},{"text":" : "},{"text":"T"},{"text":"), "},{"text":"opt"},{"ref":"Eq","text":" = "},{"ref":"Option.some","text":"Option.some"},{"text":" "},{"text":"t"},{"text":" → "},{"text":"call"},{"text":"."},{"ref":"Aeneas.Std.core.ops.function.FnOnce.call_once","text":"call_once"},{"text":" "},{"text":"f"},{"text":" "},{"text":"t"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"("},{"text":"mapping"},{"text":" "},{"text":"t"},{"text":")"}]}],"conclusion":"∃ out,\n  OptionExtContracts.map_or2 call opt f default = Aeneas.Std.Result.ok out ∧\n    out = OptionExtContracts.mapDefault mapping default opt","conclusion_segments":[{"text":"∃ "},{"text":"out"},{"text":",\n  "},{"ref":"OptionExtContracts.map_or2","text":"OptionExtContracts.map_or2"},{"text":" "},{"text":"call"},{"text":" "},{"text":"opt"},{"text":" "},{"text":"f"},{"text":" "},{"text":"default"},{"ref":"Eq","text":" = "},{"ref":"Aeneas.Std.Result.ok","text":"Aeneas.Std.Result.ok"},{"text":" "},{"text":"out"},{"ref":"And","text":" ∧\n    "},{"text":"out"},{"ref":"Eq","text":" = "},{"ref":"OptionExtContracts.mapDefault","text":"OptionExtContracts.mapDefault"},{"text":" "},{"text":"mapping"},{"text":" "},{"text":"default"},{"text":" "},{"text":"opt"}],"definitions":[{"module":"Aeneas.Std.Core.Ops","name":"Aeneas.Std.core.ops.function.FnOnce","source":{"first_line":44,"last_line":46}},{"module":"Init.Prelude","name":"Option","source":{"first_line":3047,"last_line":3058}},{"module":"Init.Prelude","name":"Eq","source":{"first_line":46,"last_line":76}},{"module":"Init.Prelude","name":"Option.some","source":{"first_line":3057,"last_line":3058}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result","source":{"first_line":67,"last_line":68}},{"module":"Aeneas.Std.Core.Ops","name":"Aeneas.Std.core.ops.function.FnOnce.call_once","source":{"first_line":46,"last_line":46}},{"module":"Aeneas.Std.Primitives","name":"Aeneas.Std.Result.ok","source":{"first_line":72,"last_line":72}},{"module":"Init.Core","name":"Exists","source":{"first_line":313,"last_line":341}},{"module":"Init.Prelude","name":"And","source":{"first_line":645,"last_line":659}},{"module":"Contracts","name":"OptionExtContracts.map_or2","source":{"first_line":20,"last_line":20}},{"module":"Contracts","name":"OptionExtContracts.mapDefault","source":{"first_line":13,"last_line":17}}],"definitions_truncated":false,"first_line":60,"last_line":68,"module":"Contracts","program":null,"program_head":null,"statement":"∀ {T : Type u_1} {V : Type u_2} {F : Type u_3} (call : Aeneas.Std.core.ops.function.FnOnce.{u_3, u_1, u_2} F T V)\n  (mapping : T → V) (opt : Option.{u_1} T) (f : F) (default : V)\n  (selected :\n    ∀ (t : T),\n      @Eq.{u_1 + 1} (Option.{u_1} T) opt (@Option.some.{u_1} T t) →\n        @Eq.{u_2 + 1} (Aeneas.Std.Result.{u_2} V)\n          (@Aeneas.Std.core.ops.function.FnOnce.call_once.{u_3, u_1, u_2} F T V call f t)\n          (@Aeneas.Std.Result.ok.{u_2} V (mapping t))),\n  @Exists.{u_2 + 1} V fun (out : V) =>\n    And\n      (@Eq.{u_2 + 1} (Aeneas.Std.Result.{u_2} V) (@OptionExtContracts.map_or2.{u_1, u_2, u_3} T V F call opt f default)\n        (@Aeneas.Std.Result.ok.{u_2} V out))\n      (@Eq.{u_2 + 1} V out (@OptionExtContracts.mapDefault.{u_1, u_2} T V mapping default opt))","theorem":"OptionExtContracts.map_or2_correct","translation_rerun":false,"version":1}

=== stderr ===