Skip to content

Unification.unify_with_current_ts gives Anomaly "File "pretyping/evarconv.ml", line 1565, characters 45-51: Assertion failed." Please report at http://rocq-prover.org/bugs/. #21652

New issue
New issue
Open
Open
Unification.unify_with_current_ts gives Anomaly "File "pretyping/evarconv.ml", line 1565, characters 45-51: Assertion failed." Please report at http://rocq-prover.org/bugs/.#21652
Labels
kind: anomalyAn uncaught exception has been raised.kind: bugAn error, flaw, fault or unintended behaviour.part: existential variablesExistential variables, also known as evars, represent as yet unknown values in a proof.part: unificationThe unification mechanism.
@JasonGross

Description

@JasonGross
JasonGross
opened on Feb 18, 2026

Description of the problem

I think both unify and Unification.unify_with_current_ts should be able to solve this problem, but at least there should not be an anomaly.

Extracted from rocq-dove on Flocq.

This is

rocq/pretyping/evarconv.ml

Lines 1561 to 1565 in 40be843

(debug_ho_unification (fun () ->
Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t));
let b, evd =
try test env !evdref c t
with e when CErrors.noncritical e -> assert false in

If I Unset Printing Records. Set Debug "ho-unification". Set Printing Depth 10000000. Set Printing Width 200., I see:

debug trace 
Debug:
[ho-unification]
  rhs env: 
  x1 : Type
  x2 : Type
  hx : Iso x1 x2
  H : IsoStatementProofForMaybeWithSorts None x1 hx
  H0 : IsoStatementProofBetween x1 x2 hx
  x3 : x1
  x4 : x2
  hx0 : rel_iso hx x3 x4
  H1 : IsoStatementProofForMaybeWithSorts None x3 hx0
  H2 : IsoStatementProofBetween x3 x4 hx0
  x5 : x1 -> Prop
  x6 : x2 -> SProp
  hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)
  H3 : IsoStatementProofForMaybeWithSorts None x5 hx1
  H4 : IsoStatementProofBetween x5 x6 hx1
  x7 : x5 x3
  x8 : x6 x4
  hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8
  H5 : IsoStatementProofForMaybeWithSorts None x7 hx2
  H6 : IsoStatementProofBetween x7 x8 hx2
  x9 : x1
  x10 : x2
  hx3 : rel_iso hx x9 x10
  H7 : IsoStatementProofForMaybeWithSorts None x9 hx3
  H8 : IsoStatementProofBetween x9 x10 hx3
  x11 : x3 = x9
  x12 : imported_Corelib__Init__Logic__eq x4 x10
  hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12
  H9 : IsoStatementProofForMaybeWithSorts None x11 hx4
  H10 : IsoStatementProofBetween x11 x12 hx4
  evar env: 
  _Goal3 := (fun (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
               (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
               (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
               (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
               (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3)
               (H8 : IsoStatementProofBetween x9 x10 hx3) (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
               (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
               (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4) =>
             ?Goal : Type)
            :
            forall (x1 x2 : Type) (hx : Iso x1 x2),
            IsoStatementProofForMaybeWithSorts None x1 hx ->
            IsoStatementProofBetween x1 x2 hx ->
            forall (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4),
            IsoStatementProofForMaybeWithSorts None x3 hx0 ->
            IsoStatementProofBetween x3 x4 hx0 ->
            forall (x5 : x1 -> Prop) (x6 : x2 -> SProp) (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)),
            IsoStatementProofForMaybeWithSorts None x5 hx1 ->
            IsoStatementProofBetween x5 x6 hx1 ->
            forall (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8),
            IsoStatementProofForMaybeWithSorts None x7 hx2 ->
            IsoStatementProofBetween x7 x8 hx2 ->
            forall (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10),
            IsoStatementProofForMaybeWithSorts None x9 hx3 ->
            IsoStatementProofBetween x9 x10 hx3 ->
            forall (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
              (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12),
            IsoStatementProofForMaybeWithSorts None x11 hx4 -> IsoStatementProofBetween x11 x12 hx4 -> Type
         : forall (x1 x2 : Type) (hx : Iso x1 x2),
           IsoStatementProofForMaybeWithSorts None x1 hx ->
           IsoStatementProofBetween x1 x2 hx ->
           forall (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4),
           IsoStatementProofForMaybeWithSorts None x3 hx0 ->
           IsoStatementProofBetween x3 x4 hx0 ->
           forall (x5 : x1 -> Prop) (x6 : x2 -> SProp) (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)),
           IsoStatementProofForMaybeWithSorts None x5 hx1 ->
           IsoStatementProofBetween x5 x6 hx1 ->
           forall (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8),
           IsoStatementProofForMaybeWithSorts None x7 hx2 ->
           IsoStatementProofBetween x7 x8 hx2 ->
           forall (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10),
           IsoStatementProofForMaybeWithSorts None x9 hx3 ->
           IsoStatementProofBetween x9 x10 hx3 ->
           forall (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
             (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12),
           IsoStatementProofForMaybeWithSorts None x11 hx4 -> IsoStatementProofBetween x11 x12 hx4 -> Type
  _Goal4 := (fun (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
               (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
               (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
               (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
               (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3)
               (H8 : IsoStatementProofBetween x9 x10 hx3) (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
               (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
               (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4) =>
             ?Goal0 : _Goal3 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
            :
            forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
              (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
              (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
              (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
              (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
              (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
              (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
              (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
            _Goal3 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10
         : forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
             (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
             (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
             (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
             (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
             (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
             (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
             (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
           _Goal3 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10
  _Goal5 := (fun (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
               (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
               (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
               (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
               (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3)
               (H8 : IsoStatementProofBetween x9 x10 hx3) (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
               (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
               (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4) =>
             ?Goal1 : Iso x1 (_Goal3 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10))
            :
            forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
              (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
              (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
              (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
              (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
              (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
              (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
              (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
            Iso x1 (_Goal3 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
         : forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
             (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
             (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
             (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
             (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
             (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
             (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
             (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
           Iso x1 (_Goal3 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
  _Goal6 := (fun (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
               (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
               (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
               (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
               (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3)
               (H8 : IsoStatementProofBetween x9 x10 hx3) (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
               (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
               (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4) =>
             ?Goal2
             :
             rel_iso (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) x9
               (_Goal4 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10))
            :
            forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
              (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
              (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
              (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
              (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
              (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
              (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
              (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
            rel_iso (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) x9
              (_Goal4 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
         : forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
             (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
             (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
             (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
             (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
             (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
             (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
             (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
           rel_iso (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) x9
             (_Goal4 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
  _Goal10 := (fun (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
                (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
                (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1)
                (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
                (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3)
                (H8 : IsoStatementProofBetween x9 x10 hx3) (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
                (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
                (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4) =>
              ?Goal3 : _Goal3 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
             :
             forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
               (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
               (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
               (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
               (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3)
               (H8 : IsoStatementProofBetween x9 x10 hx3) (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
               (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
               (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
             _Goal3 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10
          : forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
              (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
              (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
              (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
              (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
              (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
              (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
              (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
            _Goal3 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10
  _Goal7 := (fun (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
               (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
               (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
               (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
               (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3)
               (H8 : IsoStatementProofBetween x9 x10 hx3) (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
               (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
               (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4) =>
             ?Goal4
             :
             imported_Corelib__Init__Logic__eq (_Goal10 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
               (_Goal4 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10))
            :
            forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
              (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
              (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
              (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
              (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
              (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
              (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
              (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
            imported_Corelib__Init__Logic__eq (_Goal10 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
              (_Goal4 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
         : forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
             (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
             (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
             (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
             (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
             (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
             (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
             (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
           imported_Corelib__Init__Logic__eq (_Goal10 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
             (_Goal4 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
  _Goal9 := (fun (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
               (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
               (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
               (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
               (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3)
               (H8 : IsoStatementProofBetween x9 x10 hx3) (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
               (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
               (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4) =>
             ?Goal5
             :
             rel_iso (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) x3
               (_Goal10 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10))
            :
            forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
              (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
              (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
              (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
              (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
              (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
              (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
              (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
            rel_iso (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) x3
              (_Goal10 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
         : forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
             (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
             (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
             (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
             (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
             (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
             (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
             (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
           rel_iso (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) x3
             (_Goal10 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
  _Goal8 := (fun (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
               (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
               (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
               (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
               (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3)
               (H8 : IsoStatementProofBetween x9 x10 hx3) (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
               (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
               (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4) =>
             ?Goal6
             :
             rel_iso
               (relax_Iso_Ts_Ps
                  (Corelib__Init__Logic__eq_iso
                     (lift_rel_iso
                        (fun
                           x : eq (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10 x3)
                                 (_Goal10 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) =>
                         x)
                        (_Goal9 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10))
                     (lift_rel_iso
                        (fun
                           x : eq (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10 x9)
                                 (_Goal4 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) =>
                         x)
                        (_Goal6 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10))))
               x11 (_Goal7 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10))
            :
            forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
              (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
              (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
              (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
              (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
              (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
              (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
              (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
            rel_iso
              (relax_Iso_Ts_Ps
                 (Corelib__Init__Logic__eq_iso
                    (lift_rel_iso
                       (fun
                          x : eq (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10 x3)
                                (_Goal10 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) =>
                        x)
                       (_Goal9 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10))
                    (lift_rel_iso
                       (fun
                          x : eq (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10 x9)
                                (_Goal4 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) =>
                        x)
                       (_Goal6 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10))))
              x11 (_Goal7 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
         : forall (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx) (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
             (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) (x5 : x1 -> Prop) (x6 : x2 -> SProp)
             (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8)) (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
             (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8) (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2)
             (H6 : IsoStatementProofBetween x7 x8 hx2) (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3) (H8 : IsoStatementProofBetween x9 x10 hx3)
             (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
             (hx4 : rel_iso (relax_Iso_Ts_Ps (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0) (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3))) x11 x12)
             (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4),
           rel_iso
             (relax_Iso_Ts_Ps
                (Corelib__Init__Logic__eq_iso
                   (lift_rel_iso
                      (fun
                         x : eq (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10 x3)
                               (_Goal10 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) =>
                       x)
                      (_Goal9 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10))
                   (lift_rel_iso
                      (fun
                         x : eq (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10 x9)
                               (_Goal4 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) =>
                       x)
                      (_Goal6 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10))))
             x11 (_Goal7 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
  x1 : Type
  x2 : Type
  hx : Iso x1 x2
  x9 : x1
  x10 : x2
  hx3 : rel_iso hx x9 x10
  x13 : x1
  x14 : _Goal3 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10
  hx5 : rel_iso (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) x13 x14
  H11 : IsoStatementProofForMaybeWithSorts None x13 hx5
  H12 : IsoStatementProofBetween x13 x14 hx5
  x16 : imported_Corelib__Init__Logic__eq (_Goal10 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) x14
  hx6 : rel_iso
          (relax_Iso_Ts_Ps
             (Corelib__Init__Logic__eq_iso
                (lift_rel_iso
                   (fun
                      x : eq (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10 x3)
                            (_Goal10 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) =>
                    x)
                   (_Goal9 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10))
                (lift_rel_iso (fun x : eq (_Goal5 x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10 x13) x14 => x) hx5)))
          x15 x16
  H13 : IsoStatementProofForMaybeWithSorts None x15 hx6
  H14 : IsoStatementProofBetween x15 x16 hx6
Debug: [ho-unification] set holes for: H14 Build_IsoStatementProofBetween x11 ?Goal4 ?Goal6 in hx3
Debug: [ho-unification] Testing Build_IsoStatementProofBetween x11 ?Goal4 ?Goal6 against hx3
Debug: [ho-unification] succeeded
Debug: [ho-unification] Found one occurrence
         cty: Build_IsoStatementProofBetween x11 ?Goal4 ?Goal6
Debug: [ho-unification] set holes for: H13 Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 in IsoStatementProofBetween x15 ?Goal4 ?Goal6
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against IsoStatementProofBetween x15 ?Goal4 ?Goal6
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against IsoStatementProofBetween x15 ?Goal4
Debug: [ho-unification] failed
Debug:
[ho-unification]
  Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against @IsoStatementProofBetween (x3 = x9) x15
                                                                             (imported_Corelib__Init__Logic__eq
                                                                                ((fun (x1 x2 : Type) (hx : Iso x1 x2) (H : IsoStatementProofForMaybeWithSorts None x1 hx)
                                                                                    (H0 : IsoStatementProofBetween x1 x2 hx) (x3 : x1) (x4 : x2) (hx0 : rel_iso hx x3 x4)
                                                                                    (H1 : IsoStatementProofForMaybeWithSorts None x3 hx0) (H2 : IsoStatementProofBetween x3 x4 hx0) 
                                                                                    (x5 : x1 -> Prop) (x6 : x2 -> SProp) (hx1 : forall (x7 : x1) (x8 : x2), rel_iso hx x7 x8 -> Iso (x5 x7) (x6 x8))
                                                                                    (H3 : IsoStatementProofForMaybeWithSorts None x5 hx1) (H4 : IsoStatementProofBetween x5 x6 hx1) 
                                                                                    (x7 : x5 x3) (x8 : x6 x4) (hx2 : rel_iso (hx1 x3 x4 (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)) x7 x8)
                                                                                    (H5 : IsoStatementProofForMaybeWithSorts None x7 hx2) (H6 : IsoStatementProofBetween x7 x8 hx2) 
                                                                                    (x9 : x1) (x10 : x2) (hx3 : rel_iso hx x9 x10) (H7 : IsoStatementProofForMaybeWithSorts None x9 hx3)
                                                                                    (H8 : IsoStatementProofBetween x9 x10 hx3) (x11 : x3 = x9) (x12 : imported_Corelib__Init__Logic__eq x4 x10)
                                                                                    (hx4 : rel_iso
                                                                                             (relax_Iso_Ts_Ps
                                                                                                (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx x3) x4 => x) hx0)
                                                                                                   (lift_rel_iso (fun x : eq (hx x9) x10 => x) hx3)))
                                                                                             x11 x12)
                                                                                    (H9 : IsoStatementProofForMaybeWithSorts None x11 hx4) (H10 : IsoStatementProofBetween x11 x12 hx4) =>
                                                                                  ?Goal3
                                                                                  :
                                                                                  (fun (x13 x14 : Type) (hx5 : Iso x13 x14) (H11 : IsoStatementProofForMaybeWithSorts None x13 hx5)
                                                                                     (H12 : IsoStatementProofBetween x13 x14 hx5) (x15 : x13) (x16 : x14) (hx6 : rel_iso hx5 x15 x16)
                                                                                     (H13 : IsoStatementProofForMaybeWithSorts None x15 hx6) (H14 : IsoStatementProofBetween x15 x16 hx6)
                                                                                     (x17 : x13 -> Prop) (x18 : x14 -> SProp)
                                                                                     (hx7 : forall (x19 : x13) (x20 : x14), rel_iso hx5 x19 x20 -> Iso (x17 x19) (x18 x20))
                                                                                     (H15 : IsoStatementProofForMaybeWithSorts None x17 hx7) (H16 : IsoStatementProofBetween x17 x18 hx7)
                                                                                     (x19 : x17 x15) (x20 : x18 x16)
                                                                                     (hx8 : rel_iso (hx7 x15 x16 (lift_rel_iso (fun x : eq (hx5 x15) x16 => x) hx6)) x19 x20)
                                                                                     (H17 : IsoStatementProofForMaybeWithSorts None x19 hx8) (H18 : IsoStatementProofBetween x19 x20 hx8) 
                                                                                     (x21 : x13) (x22 : x14) (hx9 : rel_iso hx5 x21 x22) (H19 : IsoStatementProofForMaybeWithSorts None x21 hx9)
                                                                                     (H20 : IsoStatementProofBetween x21 x22 hx9) (x23 : x15 = x21) (x24 : imported_Corelib__Init__Logic__eq x16 x22)
                                                                                     (hx10 : rel_iso
                                                                                               (relax_Iso_Ts_Ps
                                                                                                  (Corelib__Init__Logic__eq_iso (lift_rel_iso (fun x : eq (hx5 x15) x16 => x) hx6)
                                                                                                     (lift_rel_iso (fun x : eq (hx5 x21) x22 => x) hx9)))
                                                                                               x23 x24)
                                                                                     (H21 : IsoStatementProofForMaybeWithSorts None x23 hx10) (H22 : IsoStatementProofBetween x23 x24 hx10) =>
                                                                                   ?Goal@{x1:=x13; x2:=x14; hx:=hx5; H:=H11; H0:=H12; x3:=x15; x4:=x16; hx0:=hx6; H1:=H13; H2:=H14; x5:=x17; x6:=x18;
                                                                                          hx1:=hx7; H3:=H15; H4:=H16; x7:=x19; x8:=x20; hx2:=hx8; H5:=H17; H6:=H18; x9:=x21; x10:=x22; hx3:=hx9;
                                                                                          H7:=H19; H8:=H20; x11:=x23; x12:=x24; hx4:=hx10; H9:=H21; H10:=H22}
                                                                                   :
                                                                                   Type) x1 x2 hx H H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10) x1 x2 hx H
                                                                                   H0 x3 x4 hx0 H1 H2 x5 x6 hx1 H3 H4 x7 x8 hx2 H5 H6 x9 x10 hx3 H7 H8 x11 x12 hx4 H9 H10)
                                                                                ?Goal0)
                                                                             ?Goal4
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against IsoStatementProofBetween x15
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against @IsoStatementProofBetween (x3 = x9) x15
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against IsoStatementProofBetween
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against @IsoStatementProofBetween
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against x3 = x9
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against Logic.eq x3
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against Logic.eq
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against @Logic.eq
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against x1
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against x3
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against x9
Debug: [ho-unification] failed
Debug: [ho-unification] Testing Build_IsoStatementProofForMaybeWithSorts None x11 ?Goal6 against x15
File "./bug_anomaly_unify_02.v", line 3629, characters 1-87:
Error: Anomaly "File "pretyping/evarconv.ml", line 1565, characters 45-51: Assertion failed." Please report at http://rocq-prover.org/bugs/.

Small Rocq / Coq file to reproduce the bug

https://gist.github.com/SkySkimmer/525fa6f9b9a8b0c959a1f88ebc6ae018

Version of Rocq / Coq where this bug occurs

9.1.0

Interface of Rocq / Coq where this bug occurs

rocq c

Last version of Rocq / Coq where the bug did not occur

No response

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: anomalyAn uncaught exception has been raised.kind: bugAn error, flaw, fault or unintended behaviour.part: existential variablesExistential variables, also known as evars, represent as yet unknown values in a proof.part: unificationThe unification mechanism.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions