Created
February 20, 2026 15:45
-
-
Save SkySkimmer/525fa6f9b9a8b0c959a1f88ebc6ae018 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-R" "." "IsomorphismChecker" "-top" "IsomorphismChecker.test") -*- *) | |
| (* File reduced by coq-bug-minimizer from original input, then from 3393 lines to 3304 lines, then from 3318 lines to 3490 lines, then from 3497 lines to 3327 lines, then from 3341 lines to 5219 lines, then from 5221 lines to 3351 lines, then from 3365 lines to 5967 lines, then from 5970 lines to 3356 lines, then from 3370 lines to 3523 lines, then from 3530 lines to 3386 lines, then from 3399 lines to 3384 lines, then from 3399 lines to 3364 lines, then from 3379 lines to 3366 lines, then from 3381 lines to 3364 lines, then from 3379 lines to 3364 lines *) | |
| (* coqc version 9.1+alpha compiled with OCaml 4.14.2 | |
| coqtop version 9.1+alpha | |
| Expected coqc runtime on this file: 1.603 sec | |
| Expected coqc peak memory usage on this file: 352512.0 kb *) | |
| Require Ltac2.Ltac2. | |
| Module Export IsomorphismChecker_DOT_IsomorphismDefinitions_WRAPPED. | |
| Module Export IsomorphismDefinitions. | |
| #[export] | |
| Set Universe Polymorphism. | |
| Inductive eq@{s|u|} {α:Type@{s|u}} (a:α) : α -> SProp | |
| := eq_refl : eq a a. | |
| #[local] Notation "x = y" := (eq x y) : type_scope. | |
| #[export] | |
| Set Implicit Arguments. | |
| Record Iso@{s s'|u u'|} (A : Type@{s|u}) (B : Type@{s'|u'}) := { | |
| to :> A -> B; | |
| from : B -> A; | |
| to_from : forall x, to (from x) = x; | |
| from_to : forall x, from (to x) = x; | |
| }. | |
| Record > rel_iso@{s s'|u u'|} {A B} (i : Iso@{s s'|u u'} A B) (x : A) (y : B) : SProp := { proj_rel_iso :> i.(to) x = y }. | |
| End IsomorphismDefinitions. | |
| Module Export IsomorphismChecker. | |
| Module Export IsomorphismDefinitions. | |
| Include IsomorphismChecker_DOT_IsomorphismDefinitions_WRAPPED.IsomorphismDefinitions. | |
| Ltac2 Notation shelve_unifiable := Control.shelve_unifiable (). | |
| Module Export IsomorphismChecker_DOT_EqualityLemmas_WRAPPED. | |
| Module Export EqualityLemmas. | |
| Module Export PolymorphicSpecif. | |
| Polymorphic Cumulative Variant option@{ua} {A : Type@{ua}} := Some (x : A) | None. | |
| #[global] Arguments option A : clear implicits. | |
| End PolymorphicSpecif. | |
| Definition relax_Iso_Ts_Ps@{u v u' v'|} {A : Prop} {B} (iso : Iso@{Type SProp|u v} A B) : Iso@{Prop SProp|u' v'} A B. | |
| Admitted. | |
| Definition lift_rel_iso@{s1 s'1 s2 s'2 | u1 u'1 u2 u'2 | } {A1 B1} {i1 : Iso@{s1 s'1 | u1 u'1} A1 B1} {x1 y1} {A2 B2} {i2 : Iso@{s2 s'2 | u2 u'2} A2 B2} {x2 y2} | |
| : (eq (i1 x1) y1 -> eq (i2 x2) y2) | |
| -> @rel_iso@{s1 s'1|u1 u'1} A1 B1 i1 x1 y1 -> @rel_iso@{s2 s'2|u2 u'2} A2 B2 i2 x2 y2. | |
| Admitted. | |
| End EqualityLemmas. | |
| Module Export IsomorphismChecker. | |
| Module Export EqualityLemmas. | |
| Include IsomorphismChecker_DOT_EqualityLemmas_WRAPPED.EqualityLemmas. | |
| Module Export IsomorphismChecker_DOT_IsomorphismStatementAutomationDefinitions_WRAPPED. | |
| Module Export IsomorphismStatementAutomationDefinitions. | |
| Module Export HList. | |
| Inductive hlist@{u} := | |
| | nil | |
| | const {A : Type@{u}} (hd : A) (tl : hlist) | |
| | consp {A : Prop} (hd : A) (tl : hlist) | |
| | conss {A : SProp} (hd : A) (tl : hlist). | |
| End HList. | |
| Class IsoStatementProofForMaybeWithSorts@{s s'|u u' us uo|Set < uo, us < uo} (sorts : PolymorphicSpecif.option@{uo} HList.hlist@{us}) {A : Type@{s|u}} (a : A) {isoT : Type@{s'|u'}} (iso : isoT) := {}. | |
| Class IsoStatementProofBetween@{s1 s2 s3|u1 u2 u3|} {A : Type@{s1|u1}} (a : A) {B : Type@{s2|u2}} (b : B) {isoT : Type@{s3|u3}} (iso : isoT) := {}. | |
| End IsomorphismStatementAutomationDefinitions. | |
| Module Export IsomorphismChecker. | |
| Module Export IsomorphismStatementAutomationDefinitions. | |
| Include IsomorphismChecker_DOT_IsomorphismStatementAutomationDefinitions_WRAPPED.IsomorphismStatementAutomationDefinitions. | |
| Import Ltac2.Ltac2. | |
| Parameter imported_Corelib__Init__Logic__eq : forall x : Type, x -> x -> SProp. | |
| Parameter Corelib__Init__Logic__eq_iso : forall (x1 x2 : Type) (hx : Iso x1 x2) (x3 : x1) (x4 : x2), rel_iso hx x3 x4 -> forall (x5 : x1) (x6 : x2), rel_iso hx x5 x6 -> Iso (x3 = x5) (imported_Corelib__Init__Logic__eq x4 x6). | |
| Goal True. | |
| unshelve (eassert ( | |
| let _Goal3 : (forall (x1 x2 : Type) | |
| (hx : IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| Type x1 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| Type x1 Type x2 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (x3 : x1) (x4 : x2) | |
| (hx0 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x3 x4) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x3 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x3 x4) | |
| hx0) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x3 x2 x4 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x3 x4) | |
| hx0) | |
| (x5 : forall _ : x1, Prop) (x6 : forall _ : x2, SProp) | |
| (hx1 : forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (forall _ : x1, Prop) x5 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (forall _ : x1, Prop) x5 (forall _ : x2, SProp) x6 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (x7 : x5 x3) (x8 : x6 x4) | |
| (hx2 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (x5 x3) x7 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (x5 x3) x7 (x6 x4) x8 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (x9 : x1) (x10 : x2) | |
| (hx3 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x9 x10) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x9 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x9 x10) | |
| hx3) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x9 x2 x10 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x9 x10) | |
| hx3) | |
| (x11 : @Corelib.Init.Logic.eq x1 x3 x9) | |
| (x12 : @imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (hx4 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| x12 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4), | |
| Type) := _ in | |
| let _Goal4 : (forall (x1 x2 : Type) | |
| (hx : IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| (H : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| Type x1 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (H0 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| Type x1 Type x2 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (x3 : x1) (x4 : x2) | |
| (hx0 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x3 x4) | |
| (H1 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x3 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (H2 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x3 x2 x4 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (x5 : forall _ : x1, Prop) (x6 : forall _ : x2, SProp) | |
| (hx1 : forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| (H3 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (forall _ : x1, Prop) x5 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (H4 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (forall _ : x1, Prop) x5 (forall _ : x2, SProp) x6 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (x7 : x5 x3) (x8 : x6 x4) | |
| (hx2 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| (H5 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (x5 x3) x7 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (H6 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (x5 x3) x7 (x6 x4) x8 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (x9 : x1) (x10 : x2) | |
| (hx3 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x9 x10) | |
| (H7 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x9 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (H8 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x9 x2 x10 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (x11 : @Corelib.Init.Logic.eq x1 x3 x9) | |
| (x12 : @imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (hx4 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| (H9 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4) | |
| (H10 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| x12 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| 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) := _ in | |
| let _Goal5 : (forall (x1 x2 : Type) | |
| (hx : IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| (H : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| Type x1 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (H0 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| Type x1 Type x2 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (x3 : x1) (x4 : x2) | |
| (hx0 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x3 x4) | |
| (H1 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x3 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (H2 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x3 x2 x4 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (x5 : forall _ : x1, Prop) (x6 : forall _ : x2, SProp) | |
| (hx1 : forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| (H3 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (forall _ : x1, Prop) x5 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (H4 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (forall _ : x1, Prop) x5 (forall _ : x2, SProp) x6 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (x7 : x5 x3) (x8 : x6 x4) | |
| (hx2 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| (H5 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (x5 x3) x7 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (H6 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (x5 x3) x7 (x6 x4) x8 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (x9 : x1) (x10 : x2) | |
| (hx3 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x9 x10) | |
| (H7 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x9 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (H8 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x9 x2 x10 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (x11 : @Corelib.Init.Logic.eq x1 x3 x9) | |
| (x12 : @imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (hx4 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| (H9 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4) | |
| (H10 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| x12 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4), | |
| IsomorphismChecker.IsomorphismDefinitions.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)) := _ in | |
| let _Goal6 : (forall (x1 x2 : Type) | |
| (hx : IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| (H : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| Type x1 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (H0 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| Type x1 Type x2 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (x3 : x1) (x4 : x2) | |
| (hx0 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x3 x4) | |
| (H1 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x3 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (H2 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x3 x2 x4 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (x5 : forall _ : x1, Prop) (x6 : forall _ : x2, SProp) | |
| (hx1 : forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| (H3 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (forall _ : x1, Prop) x5 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (H4 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (forall _ : x1, Prop) x5 (forall _ : x2, SProp) x6 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (x7 : x5 x3) (x8 : x6 x4) | |
| (hx2 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| (H5 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (x5 x3) x7 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (H6 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (x5 x3) x7 (x6 x4) x8 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (x9 : x1) (x10 : x2) | |
| (hx3 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x9 x10) | |
| (H7 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x9 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (H8 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x9 x2 x10 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (x11 : @Corelib.Init.Logic.eq x1 x3 x9) | |
| (x12 : @imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (hx4 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| (H9 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4) | |
| (H10 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| x12 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4), | |
| @IsomorphismChecker.IsomorphismDefinitions.rel_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) | |
| (_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)) := _ in | |
| let _Goal10 : (forall (x1 x2 : Type) | |
| (hx : IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| (H : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| Type x1 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (H0 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| Type x1 Type x2 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (x3 : x1) (x4 : x2) | |
| (hx0 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x3 x4) | |
| (H1 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x3 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (H2 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x3 x2 x4 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (x5 : forall _ : x1, Prop) (x6 : forall _ : x2, SProp) | |
| (hx1 : forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| (H3 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (forall _ : x1, Prop) x5 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (H4 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (forall _ : x1, Prop) x5 | |
| (forall _ : x2, SProp) x6 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (x7 : x5 x3) (x8 : x6 x4) | |
| (hx2 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| (H5 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (x5 x3) x7 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (H6 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (x5 x3) x7 (x6 x4) x8 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (x9 : x1) (x10 : x2) | |
| (hx3 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x9 x10) | |
| (H7 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x9 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (H8 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x9 x2 x10 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (x11 : @Corelib.Init.Logic.eq x1 x3 x9) | |
| (x12 : @imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (hx4 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| (H9 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4) | |
| (H10 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| x12 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| 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) := _ in | |
| let _Goal7 : (forall (x1 x2 : Type) | |
| (hx : IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| (H : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| Type x1 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (H0 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| Type x1 Type x2 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (x3 : x1) (x4 : x2) | |
| (hx0 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x3 x4) | |
| (H1 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x3 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (H2 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x3 x2 x4 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (x5 : forall _ : x1, Prop) (x6 : forall _ : x2, SProp) | |
| (hx1 : forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| (H3 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (forall _ : x1, Prop) x5 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (H4 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (forall _ : x1, Prop) x5 (forall _ : x2, SProp) x6 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (x7 : x5 x3) (x8 : x6 x4) | |
| (hx2 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| (H5 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (x5 x3) x7 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (H6 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (x5 x3) x7 (x6 x4) x8 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (x9 : x1) (x10 : x2) | |
| (hx3 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x9 x10) | |
| (H7 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x9 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (H8 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x9 x2 x10 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (x11 : @Corelib.Init.Logic.eq x1 x3 x9) | |
| (x12 : @imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (hx4 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| (H9 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4) | |
| (H10 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| x12 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4), | |
| @imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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)) := _ in | |
| let _Goal9 : (forall (x1 x2 : Type) | |
| (hx : IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| (H : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| Type x1 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (H0 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| Type x1 Type x2 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (x3 : x1) (x4 : x2) | |
| (hx0 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x3 x4) | |
| (H1 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x3 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (H2 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x3 x2 x4 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (x5 : forall _ : x1, Prop) (x6 : forall _ : x2, SProp) | |
| (hx1 : forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| (H3 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (forall _ : x1, Prop) x5 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (H4 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (forall _ : x1, Prop) x5 (forall _ : x2, SProp) x6 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (x7 : x5 x3) (x8 : x6 x4) | |
| (hx2 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| (H5 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (x5 x3) x7 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (H6 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (x5 x3) x7 (x6 x4) x8 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (x9 : x1) (x10 : x2) | |
| (hx3 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x9 x10) | |
| (H7 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x9 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (H8 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x9 x2 x10 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (x11 : @Corelib.Init.Logic.eq x1 x3 x9) | |
| (x12 : @imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (hx4 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| (H9 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4) | |
| (H10 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| x12 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4), | |
| @IsomorphismChecker.IsomorphismDefinitions.rel_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) | |
| (_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)) := _ in | |
| let _Goal8 : (forall (x1 x2 : Type) | |
| (hx : IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| (H : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| Type x1 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (H0 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| Type x1 Type x2 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (x3 : x1) (x4 : x2) | |
| (hx0 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x3 x4) | |
| (H1 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x3 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (H2 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x3 x2 x4 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (x5 : forall _ : x1, Prop) (x6 : forall _ : x2, SProp) | |
| (hx1 : forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| (H3 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (forall _ : x1, Prop) x5 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (H4 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (forall _ : x1, Prop) x5 (forall _ : x2, SProp) x6 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (x7 : x5 x3) (x8 : x6 x4) | |
| (hx2 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| (H5 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (x5 x3) x7 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (H6 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (x5 x3) x7 (x6 x4) x8 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (x9 : x1) (x10 : x2) | |
| (hx3 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x9 x10) | |
| (H7 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x9 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (H8 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x9 x2 x10 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (x11 : @Corelib.Init.Logic.eq x1 x3 x9) | |
| (x12 : @imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (hx4 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| (H9 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4) | |
| (H10 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| x12 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4), | |
| @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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)) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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)) | |
| (@Corelib__Init__Logic__eq_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) | |
| (_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) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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)) | |
| 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) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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)) := _ in | |
| let _Goal11 : (forall (x1 x2 : Type) | |
| (hx : IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| (H : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| Type x1 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (H0 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| Type x1 Type x2 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) | |
| hx) | |
| (x3 : x1) (x4 : x2) | |
| (hx0 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x3 x4) | |
| (H1 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x3 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (H2 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x3 x2 x4 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x3 x4) | |
| hx0) | |
| (x5 : forall _ : x1, Prop) (x6 : forall _ : x2, SProp) | |
| (hx1 : forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| (H3 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (forall _ : x1, Prop) x5 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (H4 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (forall _ : x1, Prop) x5 | |
| (forall _ : x2, SProp) x6 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x7) (x6 x8)) | |
| hx1) | |
| (x7 : x5 x3) (x8 : x6 x4) | |
| (hx2 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| (H5 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (x5 x3) x7 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (H6 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (x5 x3) x7 (x6 x4) x8 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2) | |
| (x9 : x1) (x10 : x2) | |
| (hx3 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 | |
| x2 hx x9 x10) | |
| (H7 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x9 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (H8 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x9 x2 x10 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| x1 x2 hx x9 x10) | |
| hx3) | |
| (x11 : @Corelib.Init.Logic.eq x1 x3 x9) | |
| (x12 : @imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (hx4 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| (H9 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4) | |
| (H10 : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| x12 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso | |
| x1 x2 hx x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4) | |
| (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 : @IsomorphismChecker.IsomorphismDefinitions.rel_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) | |
| (_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) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x13 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_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) | |
| (_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) | |
| hx5) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x13 | |
| (_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) | |
| x14 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_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) | |
| (_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) | |
| hx5) | |
| (x15 : @Corelib.Init.Logic.eq x1 x3 x13) | |
| (x16 : @imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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 : @IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x13) | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x13) | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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) | |
| (@Corelib__Init__Logic__eq_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) | |
| (_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) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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)) | |
| x13 x14 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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 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) | |
| (_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 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (@Corelib.Init.Logic.eq x1 x3 x13) x15 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x13) | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x13) | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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) | |
| (@Corelib__Init__Logic__eq_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) | |
| (_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) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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)) | |
| x13 x14 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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 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) | |
| (_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 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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) | |
| hx6) | |
| (_ : @IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (@Corelib.Init.Logic.eq x1 x3 x13) x15 | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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) | |
| x16 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x13) | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x13) | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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) | |
| (@Corelib__Init__Logic__eq_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) | |
| (_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) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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)) | |
| x13 x14 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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 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) | |
| (_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 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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) | |
| hx6), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso | |
| (x5 x13) (x6 x10)) := _ in | |
| forall | |
| (x1 : Type) | |
| (x2 : Type) | |
| (hx : (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2)) | |
| (H : (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| Type x1 (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) hx)) | |
| (H0 : (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| Type x1 Type x2 | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso x1 x2) hx)) | |
| (x3 : x1) | |
| (x4 : x2) | |
| (hx0 : (@IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 x2 hx x3 x4)) | |
| (H1 : (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x3 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 x2 hx x3 x4) | |
| hx0)) | |
| (H2 : (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x3 x2 x4 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 x2 hx x3 x4) | |
| hx0)) | |
| (x5 : (forall _ : x1, Prop)) | |
| (x6 : (forall _ : x2, SProp)) | |
| (hx1 : (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 x2 hx x7 | |
| x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso (x5 x7) (x6 x8))) | |
| (H3 : (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (forall _ : x1, Prop) x5 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 x2 hx | |
| x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso (x5 x7) (x6 x8)) | |
| hx1)) | |
| (H4 : (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (forall _ : x1, Prop) x5 (forall _ : x2, SProp) x6 | |
| (forall (x7 : x1) (x8 : x2) | |
| (_ : @IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 x2 hx | |
| x7 x8), | |
| IsomorphismChecker.IsomorphismDefinitions.Iso (x5 x7) (x6 x8)) | |
| hx1)) | |
| (x7 : (x5 x3)) | |
| (x8 : (x6 x4)) | |
| (hx2 : (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso x1 x2 hx x3 x4 | |
| x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to x1 x2 | |
| hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8)) | |
| (H5 : (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (x5 x3) x7 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso x1 x2 hx x3 | |
| x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to x1 | |
| x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2)) | |
| (H6 : (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (x5 x3) x7 (x6 x4) x8 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (x5 x3) (x6 x4) | |
| (hx1 x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso x1 x2 hx x3 | |
| x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to x1 | |
| x2 hx x3) | |
| x4 => | |
| x) | |
| hx0)) | |
| x7 x8) | |
| hx2)) | |
| (x9 : x1) | |
| (x10 : x2) | |
| (hx3 : (@IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 x2 hx x9 x10)) | |
| (H7 : (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x9 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 x2 hx x9 x10) | |
| hx3)) | |
| (H8 : (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| x1 x9 x2 x10 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso x1 x2 hx x9 x10) | |
| hx3)) | |
| (x11 : (@Corelib.Init.Logic.eq x1 x3 x9)) | |
| (x12 : (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10)) | |
| (hx4 : (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso x1 x2 hx x3 | |
| x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to x1 | |
| x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso x1 x2 hx x9 | |
| x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to x1 | |
| x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12)) | |
| (H9 : (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso x1 x2 hx | |
| x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso x1 x2 hx | |
| x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4)) | |
| (H10 : (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.IsoStatementProofBetween | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| x12 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| x2 x4 x10) | |
| (@Corelib__Init__Logic__eq_iso | |
| x1 x2 hx x3 x4 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso x1 x2 hx | |
| x3 x4 x1 x2 hx x3 x4 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x3) | |
| x4 => | |
| x) | |
| hx0) | |
| x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso x1 x2 hx | |
| x9 x10 x1 x2 hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| x11 x12) | |
| hx4)) | |
| , | |
| (@Corelib.Init.Logic.eq | |
| (IsomorphismChecker.IsomorphismDefinitions.Iso (x5 x9) (x6 x10)) | |
| (_Goal11 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) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to 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) | |
| (_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)) | |
| (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.Build_IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| x1 x9 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_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) | |
| (_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)) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to 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) | |
| (_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))) | |
| (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.Build_IsoStatementProofBetween | |
| x1 x9 | |
| (_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) | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_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) | |
| (_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)) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to 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) | |
| (_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) | |
| (_Goal8 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) | |
| (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.Build_IsoStatementProofForMaybeWithSorts | |
| (@IsomorphismChecker.EqualityLemmas.PolymorphicSpecif.None | |
| IsomorphismChecker.IsomorphismStatementAutomationDefinitions.HList.hlist) | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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)) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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)) | |
| (@Corelib__Init__Logic__eq_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) | |
| (_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) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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)) | |
| 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) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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)) | |
| (_Goal8 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)) | |
| (@IsomorphismChecker.IsomorphismStatementAutomationDefinitions.Build_IsoStatementProofBetween | |
| (@Corelib.Init.Logic.eq x1 x3 x9) x11 | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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)) | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.rel_iso | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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)) | |
| (@IsomorphismChecker.EqualityLemmas.relax_Iso_Ts_Ps | |
| (@Corelib.Init.Logic.eq x1 x3 x9) | |
| (@imported_Corelib__Init__Logic__eq | |
| (_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) | |
| (_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)) | |
| (@Corelib__Init__Logic__eq_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) | |
| (_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) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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)) | |
| 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) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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) | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_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) | |
| (_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) | |
| 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) | |
| (_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) | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq | |
| (_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) | |
| (@IsomorphismChecker.IsomorphismDefinitions.to | |
| 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) | |
| (_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)) | |
| (_Goal8 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))) | |
| (hx1 x9 x10 | |
| (@IsomorphismChecker.EqualityLemmas.lift_rel_iso x1 x2 hx x9 x10 x1 x2 | |
| hx x9 x10 | |
| (fun | |
| x : @IsomorphismChecker.IsomorphismDefinitions.eq x2 | |
| (@IsomorphismChecker.IsomorphismDefinitions.to x1 x2 hx x9) | |
| x10 => | |
| x) | |
| hx3))) | |
| )); cbv beta zeta; intros; cbv beta; shelve_unifiable. | |
| Import Ltac2.Ltac2 Ltac2.Printf. | |
| Set Printing Depth 10000000. | |
| Fail lazy_match! goal with | |
| | [ |- ?x = ?y ] => unify $x $y | |
| end. | |
| (* File "./bug_anomaly_unify_02.v", line 3367, characters 1-61: | |
| Error: | |
| In environment | |
| 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 | |
| Unable to unify | |
| "?r@{x9:=x9; x13:=x9; x14:=?Goal0; | |
| hx5:=lift_rel_iso | |
| (fun | |
| x : 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) => | |
| ?Goal1 | |
| : | |
| Iso x1 | |
| ((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 x9) | |
| ((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 | |
| : | |
| (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) => | |
| x) | |
| ?Goal2; | |
| H11:={| |}; H12:={| |}; x16:=?Goal4; hx6:=?Goal6; H13:={| |}; | |
| H14:={| |}}" | |
| with "hx3" (unable to find a well-typed instantiation for | |
| "?r": cannot ensure that "rel_iso hx x9 x10" is a subtype of | |
| "rel_iso hx x13 x10"). | |
| (while solving unification constraints, | |
| see flag "Solve Unification Constraints") | |
| *) | |
| Unset Printing Records. Set Debug "ho-unification". Set Printing Depth 10000000. Set Printing Width 200. | |
| lazy_match! goal with | |
| | [ |- ?x = ?y ] => Unification.unify_with_current_ts x y | |
| end. | |
| (* Error: | |
| Anomaly | |
| "File "pretyping/evarconv.ml", line 1565, characters 45-51: Assertion failed." | |
| Please report at http://rocq-prover.org/bugs/. *) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment