matita-basics-types.agda

open import Agda.Primitive
open import matita-basics-logic


data void : Set (lzero) where

match-void : (return-sort-v : Level) -> (return-type-v : (z-v : void) -> Set return-sort-v) -> (z-v : void) -> return-type-v z-v
match-void _ _ ()

void-ind : (l0-v : Level) -> (Q--v : (X-x-482-v : void) -> Set l0-v) -> (x-482-v : void) -> Q--v x-482-v
void-ind    _ _ ()

void-rect-Type4 : (l0-v : Level) -> (Q--v : (X-x-483-v : void) -> Set l0-v) -> (x-483-v : void) -> Q--v x-483-v
void-rect-Type4 _ _ ()

void-rect-Type5 : (l0-v : Level) -> (Q--v : (X-x-484-v : void) -> Set l0-v) -> (x-484-v : void) -> Q--v x-484-v
void-rect-Type5 _ _ ()

void-rect-Type3 : (l0-v : Level) -> (Q--v : (X-x-485-v : void) -> Set l0-v) -> (x-485-v : void) -> Q--v x-485-v
void-rect-Type3 _ _ ()

void-rect-Type2 : (l0-v : Level) -> (Q--v : (X-x-486-v : void) -> Set l0-v) -> (x-486-v : void) -> Q--v x-486-v
void-rect-Type2 _ _ ()

void-rect-Type1 : (l0-v : Level) -> (Q--v : (X-x-487-v : void) -> Set l0-v) -> (x-487-v : void) -> Q--v x-487-v
void-rect-Type1 _ _ ()

void-rect-Type0 : (l0-v : Level) -> (Q--v : (X-x-488-v : void) -> Set l0-v) -> (x-488-v : void) -> Q--v x-488-v
void-rect-Type0 _ _ ()


data unit : Set (lzero) where
  it : unit

match-unit : (return-sort-v : Level) -> (return-type-v : (z-v : unit) -> Set return-sort-v) -> (case-it-v : return-type-v it) -> (z-v : unit) -> return-type-v z-v
match-unit _ _ caseit it = caseit

unit-ind : (l2-v : Level) -> (Q--v : (X-x-495-v : unit) -> Set l2-v) -> (X-H-it-v : Q--v it) -> (x-495-v : unit) -> Q--v x-495-v
unit-ind _ _ caseit it = caseit

unit-rect-Type4 : (l2-v : Level) -> (Q--v : (X-x-497-v : unit) -> Set l2-v) -> (X-H-it-v : Q--v it) -> (x-497-v : unit) -> Q--v x-497-v
unit-rect-Type4 _ _ caseit it = caseit

unit-rect-Type5 : (l2-v : Level) -> (Q--v : (X-x-497-v : unit) -> Set l2-v) -> (X-H-it-v : Q--v it) -> (x-497-v : unit) -> Q--v x-497-v
unit-rect-Type5 _ _ caseit it = caseit

unit-rect-Type3 : (l2-v : Level) -> (Q--v : (X-x-497-v : unit) -> Set l2-v) -> (X-H-it-v : Q--v it) -> (x-497-v : unit) -> Q--v x-497-v
unit-rect-Type3 _ _ caseit it = caseit

unit-rect-Type2 : (l2-v : Level) -> (Q--v : (X-x-497-v : unit) -> Set l2-v) -> (X-H-it-v : Q--v it) -> (x-497-v : unit) -> Q--v x-497-v
unit-rect-Type2 _ _ caseit it = caseit

unit-rect-Type1 : (l2-v : Level) -> (Q--v : (X-x-497-v : unit) -> Set l2-v) -> (X-H-it-v : Q--v it) -> (x-497-v : unit) -> Q--v x-497-v
unit-rect-Type1 _ _ caseit it = caseit

unit-rect-Type0 : (l2-v : Level) -> (Q--v : (X-x-497-v : unit) -> Set l2-v) -> (X-H-it-v : Q--v it) -> (x-497-v : unit) -> Q--v x-497-v
unit-rect-Type0 _ _ caseit it = caseit


unit-inv-ind : (l11 : Level) -> (Hterm : unit) -> (P : (X-z906 : unit) -> Set l11) -> (X-H1 : (X-z907 : eq lzero unit Hterm it) -> P it) -> P Hterm
unit-inv-ind = λ (l11 : Level) -> λ (Hterm : unit) -> λ (P : (X-z906 : unit) -> Set l11) -> λ (H1 : (X-z907 : eq lzero unit Hterm it) -> P it) -> unit-ind l11 (λ (X-x-495 : unit) -> (X-z907 : eq lzero unit Hterm X-x-495) -> P X-x-495) H1 Hterm (refl lzero unit Hterm)

unit-inv-rect-Type4 : (l11 : Level) -> (Hterm : unit) -> (P : (X-z912 : unit) -> Set l11) -> (X-H1 : (X-z913 : eq lzero unit Hterm it) -> P it) -> P Hterm
unit-inv-rect-Type4 = λ (l11 : Level) -> λ (Hterm : unit) -> λ (P : (X-z912 : unit) -> Set l11) -> λ (H1 : (X-z913 : eq lzero unit Hterm it) -> P it) -> unit-rect-Type4 l11 (λ (X-x-497 : unit) -> (X-z913 : eq lzero unit Hterm X-x-497) -> P X-x-497) H1 Hterm (refl lzero unit Hterm)

unit-inv-rect-Type3 : (l11 : Level) -> (Hterm : unit) -> (P : (X-z918 : unit) -> Set l11) -> (X-H1 : (X-z919 : eq lzero unit Hterm it) -> P it) -> P Hterm
unit-inv-rect-Type3 = λ (l11 : Level) -> λ (Hterm : unit) -> λ (P : (X-z918 : unit) -> Set l11) -> λ (H1 : (X-z919 : eq lzero unit Hterm it) -> P it) -> unit-rect-Type3 l11 (λ (X-x-501 : unit) -> (X-z919 : eq lzero unit Hterm X-x-501) -> P X-x-501) H1 Hterm (refl lzero unit Hterm)

unit-inv-rect-Type2 : (l11 : Level) -> (Hterm : unit) -> (P : (X-z924 : unit) -> Set l11) -> (X-H1 : (X-z925 : eq lzero unit Hterm it) -> P it) -> P Hterm
unit-inv-rect-Type2 = λ (l11 : Level) -> λ (Hterm : unit) -> λ (P : (X-z924 : unit) -> Set l11) -> λ (H1 : (X-z925 : eq lzero unit Hterm it) -> P it) -> unit-rect-Type2 l11 (λ (X-x-503 : unit) -> (X-z925 : eq lzero unit Hterm X-x-503) -> P X-x-503) H1 Hterm (refl lzero unit Hterm)

unit-inv-rect-Type1 : (l11 : Level) -> (Hterm : unit) -> (P : (X-z930 : unit) -> Set l11) -> (X-H1 : (X-z931 : eq lzero unit Hterm it) -> P it) -> P Hterm
unit-inv-rect-Type1 = λ (l11 : Level) -> λ (Hterm : unit) -> λ (P : (X-z930 : unit) -> Set l11) -> λ (H1 : (X-z931 : eq lzero unit Hterm it) -> P it) -> unit-rect-Type1 l11 (λ (X-x-505 : unit) -> (X-z931 : eq lzero unit Hterm X-x-505) -> P X-x-505) H1 Hterm (refl lzero unit Hterm)

unit-inv-rect-Type0 : (l11 : Level) -> (Hterm : unit) -> (P : (X-z936 : unit) -> Set l11) -> (X-H1 : (X-z937 : eq lzero unit Hterm it) -> P it) -> P Hterm
unit-inv-rect-Type0 = λ (l11 : Level) -> λ (Hterm : unit) -> λ (P : (X-z936 : unit) -> Set l11) -> λ (H1 : (X-z937 : eq lzero unit Hterm it) -> P it) -> unit-rect-Type0 l11 (λ (X-x-507 : unit) -> (X-z937 : eq lzero unit Hterm X-x-507) -> P X-x-507) H1 Hterm (refl lzero unit Hterm)

unit-discr : (l48 : Level) -> (x : unit) -> (y : unit) -> (X-e : eq lzero unit x y) -> match-unit ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l48))) (λ (X-- : unit) -> Set ((lsuc lzero) ⊔ (lsuc l48))) (match-unit ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l48))) (λ (X-- : unit) -> Set ((lsuc lzero) ⊔ (lsuc l48))) ((P : Set l48) -> (X-z31 : P) -> P) y) x
unit-discr = λ (l48 : Level) -> λ (x : unit) -> λ (y : unit) -> λ (Deq : eq lzero unit x y) -> eq-rect-Type2 lzero ((lsuc lzero) ⊔ (lsuc l48)) unit x (λ (x-13 : unit) -> λ (X-x-14 : eq lzero unit x x-13) -> match-unit ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l48))) (λ (X-- : unit) -> Set ((lsuc lzero) ⊔ (lsuc l48))) (match-unit ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l48))) (λ (X-- : unit) -> Set ((lsuc lzero) ⊔ (lsuc l48))) ((P : Set l48) -> (X-z31 : P) -> P) x-13) x) (match-unit ((lsuc lzero) ⊔ (lsuc l48)) (λ (X-- : unit) -> match-unit ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l48))) (λ (X-0 : unit) -> Set ((lsuc lzero) ⊔ (lsuc l48))) (match-unit ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l48))) (λ (X-0 : unit) -> Set ((lsuc lzero) ⊔ (lsuc l48))) ((P : Set l48) -> (X-z31 : P) -> P) X--) X--) (λ (P : Set l48) -> λ (DH : P) -> DH) x) y Deq

data Sum (l2-v l1-v : Level) (A-v : Set l2-v) (B-v : Set l1-v) : Set (lzero ⊔ (l2-v ⊔ l1-v)) where
  inl' : (X---v : A-v) -> Sum l2-v l1-v A-v B-v
  inr' : (X---v : B-v) -> Sum l2-v l1-v A-v B-v

inl : (l3-v l0-v : Level) -> (A-v : Set l3-v) -> (B-v : Set l0-v) -> (X---v : A-v) -> Sum l3-v l0-v A-v B-v
inl _ _ _ _ = inl'

inr : (l1-v l3-v : Level) -> (A-v : Set l1-v) -> (B-v : Set l3-v) -> (X---v : B-v) -> Sum l1-v l3-v A-v B-v
inr _ _ _ _ = inr'


match-Sum : (l10-v l9-v : Level) -> (X-A-v : Set l10-v) -> (X-B-v : Set l9-v) -> (return-sort-v : Level) -> (return-type-v : (z-v : Sum l10-v l9-v X-A-v X-B-v) -> Set return-sort-v) -> (case-inl-v : (X---v : X-A-v) -> return-type-v (inl l10-v l9-v X-A-v X-B-v X---v)) -> (case-inr-v : (X---v : X-B-v) -> return-type-v (inr l10-v l9-v X-A-v X-B-v X---v)) -> (z-v : Sum l10-v l9-v X-A-v X-B-v) -> return-type-v z-v
match-Sum _ _ _ _ _ _ casel caser (inl' l) = casel l
match-Sum _ _ _ _ _ _ casel caser (inr' r) = caser r

Sum-ind : (l14-v l13-v l10-v : Level) -> (X-A-v : Set l14-v) -> (X-B-v : Set l13-v) -> (Q--v : (X-x-521-v : Sum l14-v l13-v X-A-v X-B-v) -> Set l10-v) -> (X-H-inl-v : (x-522-v : X-A-v) -> Q--v (inl l14-v l13-v X-A-v X-B-v x-522-v)) -> (X-H-inr-v : (x-523-v : X-B-v) -> Q--v (inr l14-v l13-v X-A-v X-B-v x-523-v)) -> (x-521-v : Sum l14-v l13-v X-A-v X-B-v) -> Q--v x-521-v
Sum-ind _ _ _ _ _ _ casel caser (inl' l) = casel l
Sum-ind _ _ _ _ _ _ casel caser (inr' r) = caser r

Sum-rect-Type4 : (l14-v l13-v l10-v : Level) -> (X-A-v : Set l14-v) -> (X-B-v : Set l13-v) -> (Q--v : (X-x-526-v : Sum l14-v l13-v X-A-v X-B-v) -> Set l10-v) -> (X-H-inl-v : (x-527-v : X-A-v) -> Q--v (inl l14-v l13-v X-A-v X-B-v x-527-v)) -> (X-H-inr-v : (x-528-v : X-B-v) -> Q--v (inr l14-v l13-v X-A-v X-B-v x-528-v)) -> (x-526-v : Sum l14-v l13-v X-A-v X-B-v) -> Q--v x-526-v
Sum-rect-Type4 _ _ _ _ _ _ casel caser (inl' l) = casel l
Sum-rect-Type4 _ _ _ _ _ _ casel caser (inr' r) = caser r

Sum-rect-Type5 : (l14-v l13-v l10-v : Level) -> (X-A-v : Set l14-v) -> (X-B-v : Set l13-v) -> (Q--v : (X-x-526-v : Sum l14-v l13-v X-A-v X-B-v) -> Set l10-v) -> (X-H-inl-v : (x-527-v : X-A-v) -> Q--v (inl l14-v l13-v X-A-v X-B-v x-527-v)) -> (X-H-inr-v : (x-528-v : X-B-v) -> Q--v (inr l14-v l13-v X-A-v X-B-v x-528-v)) -> (x-526-v : Sum l14-v l13-v X-A-v X-B-v) -> Q--v x-526-v
Sum-rect-Type5 _ _ _ _ _ _ casel caser (inl' l) = casel l
Sum-rect-Type5 _ _ _ _ _ _ casel caser (inr' r) = caser r

Sum-rect-Type3 : (l14-v l13-v l10-v : Level) -> (X-A-v : Set l14-v) -> (X-B-v : Set l13-v) -> (Q--v : (X-x-526-v : Sum l14-v l13-v X-A-v X-B-v) -> Set l10-v) -> (X-H-inl-v : (x-527-v : X-A-v) -> Q--v (inl l14-v l13-v X-A-v X-B-v x-527-v)) -> (X-H-inr-v : (x-528-v : X-B-v) -> Q--v (inr l14-v l13-v X-A-v X-B-v x-528-v)) -> (x-526-v : Sum l14-v l13-v X-A-v X-B-v) -> Q--v x-526-v
Sum-rect-Type3 _ _ _ _ _ _ casel caser (inl' l) = casel l
Sum-rect-Type3 _ _ _ _ _ _ casel caser (inr' r) = caser r

Sum-rect-Type2 : (l14-v l13-v l10-v : Level) -> (X-A-v : Set l14-v) -> (X-B-v : Set l13-v) -> (Q--v : (X-x-526-v : Sum l14-v l13-v X-A-v X-B-v) -> Set l10-v) -> (X-H-inl-v : (x-527-v : X-A-v) -> Q--v (inl l14-v l13-v X-A-v X-B-v x-527-v)) -> (X-H-inr-v : (x-528-v : X-B-v) -> Q--v (inr l14-v l13-v X-A-v X-B-v x-528-v)) -> (x-526-v : Sum l14-v l13-v X-A-v X-B-v) -> Q--v x-526-v
Sum-rect-Type2 _ _ _ _ _ _ casel caser (inl' l) = casel l
Sum-rect-Type2 _ _ _ _ _ _ casel caser (inr' r) = caser r

Sum-rect-Type1 : (l14-v l13-v l10-v : Level) -> (X-A-v : Set l14-v) -> (X-B-v : Set l13-v) -> (Q--v : (X-x-526-v : Sum l14-v l13-v X-A-v X-B-v) -> Set l10-v) -> (X-H-inl-v : (x-527-v : X-A-v) -> Q--v (inl l14-v l13-v X-A-v X-B-v x-527-v)) -> (X-H-inr-v : (x-528-v : X-B-v) -> Q--v (inr l14-v l13-v X-A-v X-B-v x-528-v)) -> (x-526-v : Sum l14-v l13-v X-A-v X-B-v) -> Q--v x-526-v
Sum-rect-Type1 _ _ _ _ _ _ casel caser (inl' l) = casel l
Sum-rect-Type1 _ _ _ _ _ _ casel caser (inr' r) = caser r

Sum-rect-Type0 : (l14-v l13-v l10-v : Level) -> (X-A-v : Set l14-v) -> (X-B-v : Set l13-v) -> (Q--v : (X-x-526-v : Sum l14-v l13-v X-A-v X-B-v) -> Set l10-v) -> (X-H-inl-v : (x-527-v : X-A-v) -> Q--v (inl l14-v l13-v X-A-v X-B-v x-527-v)) -> (X-H-inr-v : (x-528-v : X-B-v) -> Q--v (inr l14-v l13-v X-A-v X-B-v x-528-v)) -> (x-526-v : Sum l14-v l13-v X-A-v X-B-v) -> Q--v x-526-v
Sum-rect-Type0 _ _ _ _ _ _ casel caser (inl' l) = casel l
Sum-rect-Type0 _ _ _ _ _ _ casel caser (inr' r) = caser r




Sum-inv-ind : (l46 l45 l38 : Level) -> (x1 : Set l46) -> (x2 : Set l45) -> (Hterm : Sum l46 l45 x1 x2) -> (P : (X-z972 : Sum l46 l45 x1 x2) -> Set l38) -> (X-H1 : (x-522 : x1) -> (X-z973 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inl l46 l45 x1 x2 x-522)) -> P (inl l46 l45 x1 x2 x-522)) -> (X-H2 : (x-523 : x2) -> (X-z973 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inr l46 l45 x1 x2 x-523)) -> P (inr l46 l45 x1 x2 x-523)) -> P Hterm
Sum-inv-ind = λ (l46 l45 l38 : Level) -> λ (x1 : Set l46) -> λ (x2 : Set l45) -> λ (Hterm : Sum l46 l45 x1 x2) -> λ (P : (X-z972 : Sum l46 l45 x1 x2) -> Set l38) -> λ (H1 : (x-522 : x1) -> (X-z973 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inl l46 l45 x1 x2 x-522)) -> P (inl l46 l45 x1 x2 x-522)) -> λ (H2 : (x-523 : x2) -> (X-z973 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inr l46 l45 x1 x2 x-523)) -> P (inr l46 l45 x1 x2 x-523)) -> Sum-ind l46 l45 ((l46 ⊔ l45) ⊔ l38) x1 x2 (λ (X-x-521 : Sum l46 l45 x1 x2) -> (X-z973 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm X-x-521) -> P X-x-521) H1 H2 Hterm (refl (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm)

Sum-inv-rect-Type4 : (l46 l45 l38 : Level) -> (x1 : Set l46) -> (x2 : Set l45) -> (Hterm : Sum l46 l45 x1 x2) -> (P : (X-z978 : Sum l46 l45 x1 x2) -> Set l38) -> (X-H1 : (x-527 : x1) -> (X-z979 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inl l46 l45 x1 x2 x-527)) -> P (inl l46 l45 x1 x2 x-527)) -> (X-H2 : (x-528 : x2) -> (X-z979 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inr l46 l45 x1 x2 x-528)) -> P (inr l46 l45 x1 x2 x-528)) -> P Hterm
Sum-inv-rect-Type4 = λ (l46 l45 l38 : Level) -> λ (x1 : Set l46) -> λ (x2 : Set l45) -> λ (Hterm : Sum l46 l45 x1 x2) -> λ (P : (X-z978 : Sum l46 l45 x1 x2) -> Set l38) -> λ (H1 : (x-527 : x1) -> (X-z979 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inl l46 l45 x1 x2 x-527)) -> P (inl l46 l45 x1 x2 x-527)) -> λ (H2 : (x-528 : x2) -> (X-z979 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inr l46 l45 x1 x2 x-528)) -> P (inr l46 l45 x1 x2 x-528)) -> Sum-rect-Type4 l46 l45 ((l46 ⊔ l45) ⊔ l38) x1 x2 (λ (X-x-526 : Sum l46 l45 x1 x2) -> (X-z979 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm X-x-526) -> P X-x-526) H1 H2 Hterm (refl (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm)

Sum-inv-rect-Type3 : (l46 l45 l38 : Level) -> (x1 : Set l46) -> (x2 : Set l45) -> (Hterm : Sum l46 l45 x1 x2) -> (P : (X-z984 : Sum l46 l45 x1 x2) -> Set l38) -> (X-H1 : (x-537 : x1) -> (X-z985 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inl l46 l45 x1 x2 x-537)) -> P (inl l46 l45 x1 x2 x-537)) -> (X-H2 : (x-538 : x2) -> (X-z985 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inr l46 l45 x1 x2 x-538)) -> P (inr l46 l45 x1 x2 x-538)) -> P Hterm
Sum-inv-rect-Type3 = λ (l46 l45 l38 : Level) -> λ (x1 : Set l46) -> λ (x2 : Set l45) -> λ (Hterm : Sum l46 l45 x1 x2) -> λ (P : (X-z984 : Sum l46 l45 x1 x2) -> Set l38) -> λ (H1 : (x-537 : x1) -> (X-z985 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inl l46 l45 x1 x2 x-537)) -> P (inl l46 l45 x1 x2 x-537)) -> λ (H2 : (x-538 : x2) -> (X-z985 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inr l46 l45 x1 x2 x-538)) -> P (inr l46 l45 x1 x2 x-538)) -> Sum-rect-Type3 l46 l45 ((l46 ⊔ l45) ⊔ l38) x1 x2 (λ (X-x-536 : Sum l46 l45 x1 x2) -> (X-z985 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm X-x-536) -> P X-x-536) H1 H2 Hterm (refl (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm)

Sum-inv-rect-Type2 : (l46 l45 l38 : Level) -> (x1 : Set l46) -> (x2 : Set l45) -> (Hterm : Sum l46 l45 x1 x2) -> (P : (X-z990 : Sum l46 l45 x1 x2) -> Set l38) -> (X-H1 : (x-542 : x1) -> (X-z991 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inl l46 l45 x1 x2 x-542)) -> P (inl l46 l45 x1 x2 x-542)) -> (X-H2 : (x-543 : x2) -> (X-z991 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inr l46 l45 x1 x2 x-543)) -> P (inr l46 l45 x1 x2 x-543)) -> P Hterm
Sum-inv-rect-Type2 = λ (l46 l45 l38 : Level) -> λ (x1 : Set l46) -> λ (x2 : Set l45) -> λ (Hterm : Sum l46 l45 x1 x2) -> λ (P : (X-z990 : Sum l46 l45 x1 x2) -> Set l38) -> λ (H1 : (x-542 : x1) -> (X-z991 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inl l46 l45 x1 x2 x-542)) -> P (inl l46 l45 x1 x2 x-542)) -> λ (H2 : (x-543 : x2) -> (X-z991 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inr l46 l45 x1 x2 x-543)) -> P (inr l46 l45 x1 x2 x-543)) -> Sum-rect-Type2 l46 l45 ((l46 ⊔ l45) ⊔ l38) x1 x2 (λ (X-x-541 : Sum l46 l45 x1 x2) -> (X-z991 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm X-x-541) -> P X-x-541) H1 H2 Hterm (refl (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm)

Sum-inv-rect-Type1 : (l46 l45 l38 : Level) -> (x1 : Set l46) -> (x2 : Set l45) -> (Hterm : Sum l46 l45 x1 x2) -> (P : (X-z996 : Sum l46 l45 x1 x2) -> Set l38) -> (X-H1 : (x-547 : x1) -> (X-z997 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inl l46 l45 x1 x2 x-547)) -> P (inl l46 l45 x1 x2 x-547)) -> (X-H2 : (x-548 : x2) -> (X-z997 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inr l46 l45 x1 x2 x-548)) -> P (inr l46 l45 x1 x2 x-548)) -> P Hterm
Sum-inv-rect-Type1 = λ (l46 l45 l38 : Level) -> λ (x1 : Set l46) -> λ (x2 : Set l45) -> λ (Hterm : Sum l46 l45 x1 x2) -> λ (P : (X-z996 : Sum l46 l45 x1 x2) -> Set l38) -> λ (H1 : (x-547 : x1) -> (X-z997 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inl l46 l45 x1 x2 x-547)) -> P (inl l46 l45 x1 x2 x-547)) -> λ (H2 : (x-548 : x2) -> (X-z997 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inr l46 l45 x1 x2 x-548)) -> P (inr l46 l45 x1 x2 x-548)) -> Sum-rect-Type1 l46 l45 ((l46 ⊔ l45) ⊔ l38) x1 x2 (λ (X-x-546 : Sum l46 l45 x1 x2) -> (X-z997 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm X-x-546) -> P X-x-546) H1 H2 Hterm (refl (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm)

Sum-inv-rect-Type0 : (l46 l45 l38 : Level) -> (x1 : Set l46) -> (x2 : Set l45) -> (Hterm : Sum l46 l45 x1 x2) -> (P : (X-z1002 : Sum l46 l45 x1 x2) -> Set l38) -> (X-H1 : (x-552 : x1) -> (X-z1003 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inl l46 l45 x1 x2 x-552)) -> P (inl l46 l45 x1 x2 x-552)) -> (X-H2 : (x-553 : x2) -> (X-z1003 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inr l46 l45 x1 x2 x-553)) -> P (inr l46 l45 x1 x2 x-553)) -> P Hterm
Sum-inv-rect-Type0 = λ (l46 l45 l38 : Level) -> λ (x1 : Set l46) -> λ (x2 : Set l45) -> λ (Hterm : Sum l46 l45 x1 x2) -> λ (P : (X-z1002 : Sum l46 l45 x1 x2) -> Set l38) -> λ (H1 : (x-552 : x1) -> (X-z1003 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inl l46 l45 x1 x2 x-552)) -> P (inl l46 l45 x1 x2 x-552)) -> λ (H2 : (x-553 : x2) -> (X-z1003 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm (inr l46 l45 x1 x2 x-553)) -> P (inr l46 l45 x1 x2 x-553)) -> Sum-rect-Type0 l46 l45 ((l46 ⊔ l45) ⊔ l38) x1 x2 (λ (X-x-551 : Sum l46 l45 x1 x2) -> (X-z1003 : eq (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm X-x-551) -> P X-x-551) H1 H2 Hterm (refl (l46 ⊔ l45) (Sum l46 l45 x1 x2) Hterm)

Sum-discr : (l246 l1l186 : Level) -> (a1 : Set ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186)))) -> (a2 : Set ((lsuc lzero) ⊔ (lsuc l1l186))) -> (x : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> (y : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> (X-e : eq ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) (Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) x y) -> match-Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2 ((lsuc (lsuc lzero)) ⊔ ((lsuc (lsuc l246)) ⊔ (lsuc (lsuc l1l186)))) (λ (X-- : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> Set ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186)))) (λ (t0 : a1) -> match-Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2 ((lsuc (lsuc lzero)) ⊔ ((lsuc (lsuc l246)) ⊔ (lsuc (lsuc l1l186)))) (λ (X-- : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> Set ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186)))) (λ (u0 : a1) -> (P : Set (l246 ⊔ l1l186)) -> (X-z33 : (X-e0 : eq ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) a1 (R0 ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) a1 t0) u0) -> P) -> P) (λ (u0 : a2) -> (P : Set (l246 ⊔ l1l186)) -> P) y) (λ (t0 : a2) -> match-Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2 ((lsuc (lsuc lzero)) ⊔ ((lsuc (lsuc l246)) ⊔ (lsuc (lsuc l1l186)))) (λ (X-- : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> Set ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186)))) (λ (u0 : a1) -> (P : Set (l246 ⊔ l1l186)) -> P) (λ (u0 : a2) -> (P : Set l246) -> (X-z34 : (X-e0 : eq ((lsuc lzero) ⊔ (lsuc l1l186)) a2 (R0 ((lsuc lzero) ⊔ (lsuc l1l186)) a2 t0) u0) -> P) -> P) y) x
Sum-discr = λ (l246 l1l186 : Level) -> λ (a1 : Set ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186)))) -> λ (a2 : Set ((lsuc lzero) ⊔ (lsuc l1l186))) -> λ (x : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> λ (y : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> λ (Deq : eq ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) (Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) x y) -> eq-rect-Type2 ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) (Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) x (λ (x-13 : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> λ (X-x-14 : eq ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) (Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) x x-13) -> match-Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2 ((lsuc (lsuc lzero)) ⊔ ((lsuc (lsuc l246)) ⊔ (lsuc (lsuc l1l186)))) (λ (X-- : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> Set ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186)))) (λ (t0 : a1) -> match-Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2 ((lsuc (lsuc lzero)) ⊔ ((lsuc (lsuc l246)) ⊔ (lsuc (lsuc l1l186)))) (λ (X-- : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> Set ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186)))) (λ (u0 : a1) -> (P : Set (l246 ⊔ l1l186)) -> (X-z33 : (X-e0 : eq ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) a1 (R0 ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) a1 t0) u0) -> P) -> P) (λ (u0 : a2) -> (P : Set (l246 ⊔ l1l186)) -> P) x-13) (λ (t0 : a2) -> match-Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2 ((lsuc (lsuc lzero)) ⊔ ((lsuc (lsuc l246)) ⊔ (lsuc (lsuc l1l186)))) (λ (X-- : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> Set ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186)))) (λ (u0 : a1) -> (P : Set (l246 ⊔ l1l186)) -> P) (λ (u0 : a2) -> (P : Set l246) -> (X-z34 : (X-e0 : eq ((lsuc lzero) ⊔ (lsuc l1l186)) a2 (R0 ((lsuc lzero) ⊔ (lsuc l1l186)) a2 t0) u0) -> P) -> P) x-13) x) (match-Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2 ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) (λ (X-- : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> match-Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2 ((lsuc (lsuc lzero)) ⊔ ((lsuc (lsuc l246)) ⊔ (lsuc (lsuc l1l186)))) (λ (X-0 : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> Set ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186)))) (λ (t0 : a1) -> match-Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2 ((lsuc (lsuc lzero)) ⊔ ((lsuc (lsuc l246)) ⊔ (lsuc (lsuc l1l186)))) (λ (X-0 : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> Set ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186)))) (λ (u0 : a1) -> (P : Set (l246 ⊔ l1l186)) -> (X-z33 : (X-e0 : eq ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) a1 (R0 ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) a1 t0) u0) -> P) -> P) (λ (u0 : a2) -> (P : Set (l246 ⊔ l1l186)) -> P) X--) (λ (t0 : a2) -> match-Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2 ((lsuc (lsuc lzero)) ⊔ ((lsuc (lsuc l246)) ⊔ (lsuc (lsuc l1l186)))) (λ (X-0 : Sum ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) ((lsuc lzero) ⊔ (lsuc l1l186)) a1 a2) -> Set ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186)))) (λ (u0 : a1) -> (P : Set (l246 ⊔ l1l186)) -> P) (λ (u0 : a2) -> (P : Set l246) -> (X-z34 : (X-e0 : eq ((lsuc lzero) ⊔ (lsuc l1l186)) a2 (R0 ((lsuc lzero) ⊔ (lsuc l1l186)) a2 t0) u0) -> P) -> P) X--) X--) (λ (a0 : a1) -> λ (P : Set (lzero ⊔ (l246 ⊔ l1l186))) -> λ (DH : (X-e0 : eq ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) a1 (R0 ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) a1 a0) a0) -> P) -> DH (refl ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) a1 (R0 ((lsuc lzero) ⊔ ((lsuc l246) ⊔ (lsuc l1l186))) a1 a0))) (λ (a0 : a2) -> λ (P : Set l246) -> λ (DH : (X-e0 : eq ((lsuc lzero) ⊔ (lsuc l1l186)) a2 (R0 ((lsuc lzero) ⊔ (lsuc l1l186)) a2 a0) a0) -> P) -> DH (refl ((lsuc lzero) ⊔ (lsuc l1l186)) a2 (R0 ((lsuc lzero) ⊔ (lsuc l1l186)) a2 a0))) x) y Deq


data option (l1-v : Level) (X-A-v : Set l1-v) : Set l1-v where
  None' : option l1-v X-A-v
  Some' : X-A-v -> option l1-v X-A-v

None : (l1-v : Level) -> (A-v : Set l1-v) -> option l1-v A-v
None _ _ = None'

Some : (l2-v : Level) -> (A-v : Set l2-v) -> (X---v : A-v) -> option l2-v A-v
Some _ _ = Some'

match-option : (l6-v : Level) -> (X-A-v : Set l6-v) -> (return-sort-v : Level) -> (return-type-v : (z-v : option l6-v X-A-v) -> Set return-sort-v) -> (case-None-v : return-type-v (None l6-v X-A-v)) -> (case-Some-v : (X---v : X-A-v) -> return-type-v (Some l6-v X-A-v X---v)) -> (z-v : option l6-v X-A-v) -> return-type-v z-v
match-option _ _ _ _ casenone casesome None' = casenone
match-option _ _ _ _ casenone casesome (Some' x) = casesome x

option-ind : (l10-v l7-v : Level) -> (X-A-v : Set l10-v) -> (Q--v : (X-x-586-v : option l10-v X-A-v) -> Set l7-v) -> (X-H-None-v : Q--v (None l10-v X-A-v)) -> (X-H-Some-v : (x-587-v : X-A-v) -> Q--v (Some l10-v X-A-v x-587-v)) -> (x-586-v : option l10-v X-A-v) -> Q--v x-586-v
option-ind _ _ _ _ casenone casesome None' = casenone
option-ind _ _ _ _ casenone casesome (Some' x) = casesome x

option-rect-Type4 : (l10-v l7-v : Level) -> (X-A-v : Set l10-v) -> (Q--v : (X-x-590-v : option l10-v X-A-v) -> Set l7-v) -> (X-H-None-v : Q--v (None l10-v X-A-v)) -> (X-H-Some-v : (x-591-v : X-A-v) -> Q--v (Some l10-v X-A-v x-591-v)) -> (x-590-v : option l10-v X-A-v) -> Q--v x-590-v
option-rect-Type4 _ _ _ _ casenone casesome None' = casenone
option-rect-Type4 _ _ _ _ casenone casesome (Some' x) = casesome x

option-rect-Type5 : (l10-v l7-v : Level) -> (X-A-v : Set l10-v) -> (Q--v : (X-x-590-v : option l10-v X-A-v) -> Set l7-v) -> (X-H-None-v : Q--v (None l10-v X-A-v)) -> (X-H-Some-v : (x-591-v : X-A-v) -> Q--v (Some l10-v X-A-v x-591-v)) -> (x-590-v : option l10-v X-A-v) -> Q--v x-590-v
option-rect-Type5 _ _ _ _ casenone casesome None' = casenone
option-rect-Type5 _ _ _ _ casenone casesome (Some' x) = casesome x

option-rect-Type3 : (l10-v l7-v : Level) -> (X-A-v : Set l10-v) -> (Q--v : (X-x-590-v : option l10-v X-A-v) -> Set l7-v) -> (X-H-None-v : Q--v (None l10-v X-A-v)) -> (X-H-Some-v : (x-591-v : X-A-v) -> Q--v (Some l10-v X-A-v x-591-v)) -> (x-590-v : option l10-v X-A-v) -> Q--v x-590-v
option-rect-Type3 _ _ _ _ casenone casesome None' = casenone
option-rect-Type3 _ _ _ _ casenone casesome (Some' x) = casesome x

option-rect-Type2 : (l10-v l7-v : Level) -> (X-A-v : Set l10-v) -> (Q--v : (X-x-590-v : option l10-v X-A-v) -> Set l7-v) -> (X-H-None-v : Q--v (None l10-v X-A-v)) -> (X-H-Some-v : (x-591-v : X-A-v) -> Q--v (Some l10-v X-A-v x-591-v)) -> (x-590-v : option l10-v X-A-v) -> Q--v x-590-v
option-rect-Type2 _ _ _ _ casenone casesome None' = casenone
option-rect-Type2 _ _ _ _ casenone casesome (Some' x) = casesome x

option-rect-Type1 : (l10-v l7-v : Level) -> (X-A-v : Set l10-v) -> (Q--v : (X-x-590-v : option l10-v X-A-v) -> Set l7-v) -> (X-H-None-v : Q--v (None l10-v X-A-v)) -> (X-H-Some-v : (x-591-v : X-A-v) -> Q--v (Some l10-v X-A-v x-591-v)) -> (x-590-v : option l10-v X-A-v) -> Q--v x-590-v
option-rect-Type1 _ _ _ _ casenone casesome None' = casenone
option-rect-Type1 _ _ _ _ casenone casesome (Some' x) = casesome x

option-rect-Type0 : (l10-v l7-v : Level) -> (X-A-v : Set l10-v) -> (Q--v : (X-x-590-v : option l10-v X-A-v) -> Set l7-v) -> (X-H-None-v : Q--v (None l10-v X-A-v)) -> (X-H-Some-v : (x-591-v : X-A-v) -> Q--v (Some l10-v X-A-v x-591-v)) -> (x-590-v : option l10-v X-A-v) -> Q--v x-590-v
option-rect-Type0 _ _ _ _ casenone casesome None' = casenone
option-rect-Type0 _ _ _ _ casenone casesome (Some' x) = casesome x



option-inv-ind : (l31 l26 : Level) -> (x1 : Set l31) -> (Hterm : option l31 x1) -> (P : (X-z1038 : option l31 x1) -> Set l26) -> (X-H1 : (X-z1039 : eq l31 (option l31 x1) Hterm (None l31 x1)) -> P (None l31 x1)) -> (X-H2 : (x-587 : x1) -> (X-z1039 : eq l31 (option l31 x1) Hterm (Some l31 x1 x-587)) -> P (Some l31 x1 x-587)) -> P Hterm
option-inv-ind = λ (l31 l26 : Level) -> λ (x1 : Set l31) -> λ (Hterm : option l31 x1) -> λ (P : (X-z1038 : option l31 x1) -> Set l26) -> λ (H1 : (X-z1039 : eq l31 (option l31 x1) Hterm (None l31 x1)) -> P (None l31 x1)) -> λ (H2 : (x-587 : x1) -> (X-z1039 : eq l31 (option l31 x1) Hterm (Some l31 x1 x-587)) -> P (Some l31 x1 x-587)) -> option-ind l31 (l31 ⊔ l26) x1 (λ (X-x-586 : option l31 x1) -> (X-z1039 : eq l31 (option l31 x1) Hterm X-x-586) -> P X-x-586) H1 H2 Hterm (refl l31 (option l31 x1) Hterm)

option-inv-rect-Type4 : (l31 l26 : Level) -> (x1 : Set l31) -> (Hterm : option l31 x1) -> (P : (X-z1044 : option l31 x1) -> Set l26) -> (X-H1 : (X-z1045 : eq l31 (option l31 x1) Hterm (None l31 x1)) -> P (None l31 x1)) -> (X-H2 : (x-591 : x1) -> (X-z1045 : eq l31 (option l31 x1) Hterm (Some l31 x1 x-591)) -> P (Some l31 x1 x-591)) -> P Hterm
option-inv-rect-Type4 = λ (l31 l26 : Level) -> λ (x1 : Set l31) -> λ (Hterm : option l31 x1) -> λ (P : (X-z1044 : option l31 x1) -> Set l26) -> λ (H1 : (X-z1045 : eq l31 (option l31 x1) Hterm (None l31 x1)) -> P (None l31 x1)) -> λ (H2 : (x-591 : x1) -> (X-z1045 : eq l31 (option l31 x1) Hterm (Some l31 x1 x-591)) -> P (Some l31 x1 x-591)) -> option-rect-Type4 l31 (l31 ⊔ l26) x1 (λ (X-x-590 : option l31 x1) -> (X-z1045 : eq l31 (option l31 x1) Hterm X-x-590) -> P X-x-590) H1 H2 Hterm (refl l31 (option l31 x1) Hterm)

option-inv-rect-Type3 : (l31 l26 : Level) -> (x1 : Set l31) -> (Hterm : option l31 x1) -> (P : (X-z1050 : option l31 x1) -> Set l26) -> (X-H1 : (X-z1051 : eq l31 (option l31 x1) Hterm (None l31 x1)) -> P (None l31 x1)) -> (X-H2 : (x-599 : x1) -> (X-z1051 : eq l31 (option l31 x1) Hterm (Some l31 x1 x-599)) -> P (Some l31 x1 x-599)) -> P Hterm
option-inv-rect-Type3 = λ (l31 l26 : Level) -> λ (x1 : Set l31) -> λ (Hterm : option l31 x1) -> λ (P : (X-z1050 : option l31 x1) -> Set l26) -> λ (H1 : (X-z1051 : eq l31 (option l31 x1) Hterm (None l31 x1)) -> P (None l31 x1)) -> λ (H2 : (x-599 : x1) -> (X-z1051 : eq l31 (option l31 x1) Hterm (Some l31 x1 x-599)) -> P (Some l31 x1 x-599)) -> option-rect-Type3 l31 (l31 ⊔ l26) x1 (λ (X-x-598 : option l31 x1) -> (X-z1051 : eq l31 (option l31 x1) Hterm X-x-598) -> P X-x-598) H1 H2 Hterm (refl l31 (option l31 x1) Hterm)

option-inv-rect-Type2 : (l31 l26 : Level) -> (x1 : Set l31) -> (Hterm : option l31 x1) -> (P : (X-z1056 : option l31 x1) -> Set l26) -> (X-H1 : (X-z1057 : eq l31 (option l31 x1) Hterm (None l31 x1)) -> P (None l31 x1)) -> (X-H2 : (x-603 : x1) -> (X-z1057 : eq l31 (option l31 x1) Hterm (Some l31 x1 x-603)) -> P (Some l31 x1 x-603)) -> P Hterm
option-inv-rect-Type2 = λ (l31 l26 : Level) -> λ (x1 : Set l31) -> λ (Hterm : option l31 x1) -> λ (P : (X-z1056 : option l31 x1) -> Set l26) -> λ (H1 : (X-z1057 : eq l31 (option l31 x1) Hterm (None l31 x1)) -> P (None l31 x1)) -> λ (H2 : (x-603 : x1) -> (X-z1057 : eq l31 (option l31 x1) Hterm (Some l31 x1 x-603)) -> P (Some l31 x1 x-603)) -> option-rect-Type2 l31 (l31 ⊔ l26) x1 (λ (X-x-602 : option l31 x1) -> (X-z1057 : eq l31 (option l31 x1) Hterm X-x-602) -> P X-x-602) H1 H2 Hterm (refl l31 (option l31 x1) Hterm)

option-inv-rect-Type1 : (l31 l26 : Level) -> (x1 : Set l31) -> (Hterm : option l31 x1) -> (P : (X-z1062 : option l31 x1) -> Set l26) -> (X-H1 : (X-z1063 : eq l31 (option l31 x1) Hterm (None l31 x1)) -> P (None l31 x1)) -> (X-H2 : (x-607 : x1) -> (X-z1063 : eq l31 (option l31 x1) Hterm (Some l31 x1 x-607)) -> P (Some l31 x1 x-607)) -> P Hterm
option-inv-rect-Type1 = λ (l31 l26 : Level) -> λ (x1 : Set l31) -> λ (Hterm : option l31 x1) -> λ (P : (X-z1062 : option l31 x1) -> Set l26) -> λ (H1 : (X-z1063 : eq l31 (option l31 x1) Hterm (None l31 x1)) -> P (None l31 x1)) -> λ (H2 : (x-607 : x1) -> (X-z1063 : eq l31 (option l31 x1) Hterm (Some l31 x1 x-607)) -> P (Some l31 x1 x-607)) -> option-rect-Type1 l31 (l31 ⊔ l26) x1 (λ (X-x-606 : option l31 x1) -> (X-z1063 : eq l31 (option l31 x1) Hterm X-x-606) -> P X-x-606) H1 H2 Hterm (refl l31 (option l31 x1) Hterm)

option-inv-rect-Type0 : (l31 l26 : Level) -> (x1 : Set l31) -> (Hterm : option l31 x1) -> (P : (X-z1068 : option l31 x1) -> Set l26) -> (X-H1 : (X-z1069 : eq l31 (option l31 x1) Hterm (None l31 x1)) -> P (None l31 x1)) -> (X-H2 : (x-611 : x1) -> (X-z1069 : eq l31 (option l31 x1) Hterm (Some l31 x1 x-611)) -> P (Some l31 x1 x-611)) -> P Hterm
option-inv-rect-Type0 = λ (l31 l26 : Level) -> λ (x1 : Set l31) -> λ (Hterm : option l31 x1) -> λ (P : (X-z1068 : option l31 x1) -> Set l26) -> λ (H1 : (X-z1069 : eq l31 (option l31 x1) Hterm (None l31 x1)) -> P (None l31 x1)) -> λ (H2 : (x-611 : x1) -> (X-z1069 : eq l31 (option l31 x1) Hterm (Some l31 x1 x-611)) -> P (Some l31 x1 x-611)) -> option-rect-Type0 l31 (l31 ⊔ l26) x1 (λ (X-x-610 : option l31 x1) -> (X-z1069 : eq l31 (option l31 x1) Hterm X-x-610) -> P X-x-610) H1 H2 Hterm (refl l31 (option l31 x1) Hterm)

option-discr : (l174 : Level) -> (a1 : Set (lzero)) -> (x : option lzero a1) -> (y : option lzero a1) -> (X-e : eq lzero (option lzero a1) x y) -> match-option lzero a1 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l174))) (λ (X-- : option lzero a1) -> Set ((lsuc lzero) ⊔ (lsuc l174))) (match-option lzero a1 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l174))) (λ (X-- : option lzero a1) -> Set ((lsuc lzero) ⊔ (lsuc l174))) ((P : Set l174) -> (X-z37 : P) -> P) (λ (u0 : a1) -> (P : Set l174) -> P) y) (λ (t0 : a1) -> match-option lzero a1 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l174))) (λ (X-- : option lzero a1) -> Set ((lsuc lzero) ⊔ (lsuc l174))) ((P : Set l174) -> P) (λ (u0 : a1) -> (P : Set l174) -> (X-z38 : (X-e0 : eq lzero a1 (R0 lzero a1 t0) u0) -> P) -> P) y) x
option-discr = λ (l174 : Level) -> λ (a1 : Set (lzero)) -> λ (x : option lzero a1) -> λ (y : option lzero a1) -> λ (Deq : eq lzero (option lzero a1) x y) -> eq-rect-Type2 lzero ((lsuc lzero) ⊔ (lsuc l174)) (option lzero a1) x (λ (x-13 : option lzero a1) -> λ (X-x-14 : eq lzero (option lzero a1) x x-13) -> match-option lzero a1 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l174))) (λ (X-- : option lzero a1) -> Set ((lsuc lzero) ⊔ (lsuc l174))) (match-option lzero a1 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l174))) (λ (X-- : option lzero a1) -> Set ((lsuc lzero) ⊔ (lsuc l174))) ((P : Set l174) -> (X-z37 : P) -> P) (λ (u0 : a1) -> (P : Set l174) -> P) x-13) (λ (t0 : a1) -> match-option lzero a1 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l174))) (λ (X-- : option lzero a1) -> Set ((lsuc lzero) ⊔ (lsuc l174))) ((P : Set l174) -> P) (λ (u0 : a1) -> (P : Set l174) -> (X-z38 : (X-e0 : eq lzero a1 (R0 lzero a1 t0) u0) -> P) -> P) x-13) x) (match-option lzero a1 ((lsuc lzero) ⊔ (lsuc l174)) (λ (X-- : option lzero a1) -> match-option lzero a1 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l174))) (λ (X-0 : option lzero a1) -> Set ((lsuc lzero) ⊔ (lsuc l174))) (match-option lzero a1 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l174))) (λ (X-0 : option lzero a1) -> Set ((lsuc lzero) ⊔ (lsuc l174))) ((P : Set l174) -> (X-z37 : P) -> P) (λ (u0 : a1) -> (P : Set l174) -> P) X--) (λ (t0 : a1) -> match-option lzero a1 ((lsuc (lsuc lzero)) ⊔ (lsuc (lsuc l174))) (λ (X-0 : option lzero a1) -> Set ((lsuc lzero) ⊔ (lsuc l174))) ((P : Set l174) -> P) (λ (u0 : a1) -> (P : Set l174) -> (X-z38 : (X-e0 : eq lzero a1 (R0 lzero a1 t0) u0) -> P) -> P) X--) X--) (λ (P : Set l174) -> λ (DH : P) -> DH) (λ (a0 : a1) -> λ (P : Set l174) -> λ (DH : (X-e0 : eq lzero a1 (R0 lzero a1 a0) a0) -> P) -> DH (refl lzero a1 (R0 lzero a1 a0))) x) y Deq

option-map : (l13 l12 : Level) -> (A : Set l13) -> (B : Set l12) -> (X-- : (X-- : A) -> B) -> (X--1 : option l13 A) -> option l12 B
option-map = λ (l13 l12 : Level) -> λ (A : Set l13) -> λ (B : Set l12) -> λ (f : (X-- : A) -> B) -> λ (o : option l13 A) -> match-option l13 A l12 (λ (X-- : option l13 A) -> option l12 B) (None l12 B) (λ (a : A) -> Some l12 B (f a)) o

option-map-none : (l50 : Level) -> (A : Set l50) -> (B : Set (lzero)) -> (f : (X-- : A) -> B) -> (x : option l50 A) -> (X-- : eq lzero (option lzero B) (option-map l50 lzero A B f x) (None lzero B)) -> eq l50 (option l50 A) x (None l50 A)
option-map-none = λ (l50 : Level) -> λ (A : Set l50) -> λ (B : Set (lzero)) -> λ (f : (X-- : A) -> B) -> λ (X-clearme : option l50 A) -> match-option l50 A l50 (λ (X-- : option l50 A) -> (X--1 : eq lzero (option lzero B) (option-map l50 lzero A B f X--) (None lzero B)) -> eq l50 (option l50 A) X-- (None l50 A)) (λ (auto : eq lzero (option lzero B) (option-map l50 lzero A B f (None l50 A)) (None lzero B)) -> refl l50 (option l50 A) (None l50 A)) (λ (a : A) -> λ (E : eq lzero (option lzero B) (option-map l50 lzero A B f (Some l50 A a)) (None lzero B)) -> option-discr l50 B (Some lzero B (f a)) (None lzero B) E (eq l50 (option l50 A) (Some l50 A a) (None l50 A))) X-clearme

option-map-some : (l146 : Level) -> (A : Set l146) -> (B : Set (lzero)) -> (f : (X-- : A) -> B) -> (x : option l146 A) -> (v : B) -> (X-- : eq lzero (option lzero B) (option-map l146 lzero A B f x) (Some lzero B v)) -> ex l146 l146 A (λ (y : A) -> And l146 lzero (eq l146 (option l146 A) x (Some l146 A y)) (eq lzero B (f y) v))
option-map-some = λ (l146 : Level) -> λ (A : Set l146) -> λ (B : Set (lzero)) -> λ (f : (X-- : A) -> B) -> λ (X-clearme : option l146 A) -> match-option l146 A l146 (λ (X-- : option l146 A) -> (v : B) -> (X--1 : eq lzero (option lzero B) (option-map l146 lzero A B f X--) (Some lzero B v)) -> ex l146 l146 A (λ (y : A) -> And l146 lzero (eq l146 (option l146 A) X-- (Some l146 A y)) (eq lzero B (f y) v))) (λ (v : B) -> λ (E : eq lzero (option lzero B) (None lzero B) (Some lzero B v)) -> option-discr l146 B (None lzero B) (Some lzero B v) E (ex l146 l146 A (λ (y : A) -> And l146 lzero (eq l146 (option l146 A) (None l146 A) (Some l146 A y)) (eq lzero B (f y) v)))) (λ (y : A) -> λ (v : B) -> λ (E : eq lzero (option lzero B) (Some lzero B (f y)) (Some lzero B v)) -> ex-intro l146 l146 A (λ (y0 : A) -> And l146 lzero (eq l146 (option l146 A) (Some l146 A y) (Some l146 A y0)) (eq lzero B (f y0) v)) y (option-discr l146 B (Some lzero B (f y)) (Some lzero B v) E (And l146 lzero (eq l146 (option l146 A) (Some l146 A y) (Some l146 A y)) (eq lzero B (f y) v)) (λ (e0 : eq lzero B (R0 lzero B (f y)) v) -> eq-ind lzero l146 B (f y) (λ (x-1 : B) -> λ (X-x-2 : eq lzero B (f y) x-1) -> (X-- : eq lzero (option lzero B) (Some lzero B (f y)) (Some lzero B x-1)) -> And l146 lzero (eq l146 (option l146 A) (Some l146 A y) (Some l146 A y)) (eq lzero B (f y) x-1)) (λ (E0 : eq lzero (option lzero B) (Some lzero B (f y)) (Some lzero B (f y))) -> streicherK lzero l146 (option lzero B) (Some lzero B (f y)) (λ (X-- : eq lzero (option lzero B) (Some lzero B (f y)) (Some lzero B (f y))) -> And l146 lzero (eq l146 (option l146 A) (Some l146 A y) (Some l146 A y)) (eq lzero B (f y) (f y))) (conj l146 lzero (eq l146 (option l146 A) (Some l146 A y) (Some l146 A y)) (eq lzero B (f y) (f y)) (refl l146 (option l146 A) (Some l146 A y)) (refl lzero B (f y))) E0) v e0 E))) X-clearme

option-map-def : (l11 l10 : Level) -> (A : Set l11) -> (B : Set l10) -> (X-- : (X-- : A) -> B) -> (X--1 : B) -> (X--2 : option l11 A) -> B
option-map-def = λ (l11 l10 : Level) -> λ (A : Set l11) -> λ (B : Set l10) -> λ (f : (X-- : A) -> B) -> λ (d : B) -> λ (o : option l11 A) -> match-option l11 A l10 (λ (X-- : option l11 A) -> B) d (λ (a : A) -> f a) o

refute-none-by-refl : (l172 l161 l157 l175 : Level) -> (A : Set l172) -> (B : Set l161) -> (P : (X-- : A) -> B) -> (Q : (X-- : B) -> Set l157) -> (x : option l172 A) -> (H : (X-- : eq l172 (option l172 A) x (None l172 A)) -> False l175) -> (X-- : (v : A) -> (X-- : eq l172 (option l172 A) x (Some l172 A v)) -> Q (P v)) -> Q (match-option l172 A (l172 ⊔ l161) (λ (y : option l172 A) -> (X--1 : eq l172 (option l172 A) x y) -> B) (λ (E : eq l172 (option l172 A) x (None l172 A)) -> match-False l175 l161 (λ (X-0 : False l175) -> B) (H E)) (λ (v : A) -> λ (X-0 : eq l172 (option l172 A) x (Some l172 A v)) -> P v) x (refl l172 (option l172 A) x))
refute-none-by-refl = λ (l172 l161 l157 l175 : Level) -> λ (A : Set l172) -> λ (B : Set l161) -> λ (P : (X-- : A) -> B) -> λ (Q : (X-- : B) -> Set l157) -> λ (X-clearme : option l172 A) -> match-option l172 A ((l175 ⊔ l172) ⊔ l157) (λ (X-- : option l172 A) -> (H : (X--1 : eq l172 (option l172 A) X-- (None l172 A)) -> False l175) -> (X--1 : (v : A) -> (X--1 : eq l172 (option l172 A) X-- (Some l172 A v)) -> Q (P v)) -> Q (match-option l172 A (l172 ⊔ l161) (λ (y : option l172 A) -> (X--2 : eq l172 (option l172 A) X-- y) -> B) (λ (E : eq l172 (option l172 A) X-- (None l172 A)) -> match-False l175 l161 (λ (X-0 : False l175) -> B) (H E)) (λ (v : A) -> λ (X-0 : eq l172 (option l172 A) X-- (Some l172 A v)) -> P v) X-- (refl l172 (option l172 A) X--))) (λ (H : (X-- : eq l172 (option l172 A) (None l172 A) (None l172 A)) -> False l175) -> match-False l175 (l172 ⊔ l157) (λ (X-- : False l175) -> (X--1 : (v : A) -> (X--1 : eq l172 (option l172 A) (None l172 A) (Some l172 A v)) -> Q (P v)) -> Q (match-option l172 A (l172 ⊔ l161) (λ (y : option l172 A) -> (X--2 : eq l172 (option l172 A) (None l172 A) y) -> B) (λ (E : eq l172 (option l172 A) (None l172 A) (None l172 A)) -> match-False l175 l161 (λ (X-0 : False l175) -> B) (H E)) (λ (v : A) -> λ (X-0 : eq l172 (option l172 A) (None l172 A) (Some l172 A v)) -> P v) (None l172 A) (refl l172 (option l172 A) (None l172 A)))) (H (refl l172 (option l172 A) (None l172 A)))) (λ (a : A) -> λ (H : (X-- : eq l172 (option l172 A) (Some l172 A a) (None l172 A)) -> False l175) -> λ (p : (v : A) -> (X-- : eq l172 (option l172 A) (Some l172 A a) (Some l172 A v)) -> Q (P v)) -> p a (refl l172 (option l172 A) (Some l172 A a))) X-clearme


data DPair (l2-v l1-v : Level) (A-v : Set l2-v) (f-v : (X---v : A-v) -> Set l1-v) : Set (lzero ⊔ (l2-v ⊔ l1-v)) where
  mk-DPair' : (dpi1-v : A-v) -> (X-dpi2-v : f-v dpi1-v) -> DPair l2-v l1-v A-v f-v

mk-DPair : (l1-v l3-v : Level) -> (A-v : Set l1-v) -> (f-v : (X---v : A-v) -> Set l3-v) -> (dpi1-v : A-v) -> (X-dpi2-v : f-v dpi1-v) -> DPair l1-v l3-v A-v f-v
mk-DPair _ _ _ _ = mk-DPair'

match-DPair : (l8-v l7-v : Level) -> (A-v : Set l8-v) -> (X-f-v : (X---v : A-v) -> Set l7-v) -> (return-sort-v : Level) -> (return-type-v : (z-v : DPair l8-v l7-v A-v X-f-v) -> Set return-sort-v) -> (case-mk-DPair-v : (dpi1-v : A-v) -> (X-dpi2-v : X-f-v dpi1-v) -> return-type-v (mk-DPair l8-v l7-v A-v X-f-v dpi1-v X-dpi2-v)) -> (z-v : DPair l8-v l7-v A-v X-f-v) -> return-type-v z-v
match-DPair _ _ _ _ _ _ casemk (mk-DPair' x px) = casemk x px

DPair-ind : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-638-v : DPair l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-DPair-v : (dpi1-v : A-v) -> (X-dpi2-v : X-f-v dpi1-v) -> Q--v (mk-DPair l11-v l10-v A-v X-f-v dpi1-v X-dpi2-v)) -> (x-638-v : DPair l11-v l10-v A-v X-f-v) -> Q--v x-638-v
DPair-ind _ _ _ _ _ _ casemk (mk-DPair' x px) = casemk x px

DPair-rect-Type5 : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-640-v : DPair l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-DPair-v : (dpi1-v : A-v) -> (X-dpi2-v : X-f-v dpi1-v) -> Q--v (mk-DPair l11-v l10-v A-v X-f-v dpi1-v X-dpi2-v)) -> (x-640-v : DPair l11-v l10-v A-v X-f-v) -> Q--v x-640-v
DPair-rect-Type5 _ _ _ _ _ _ casemk (mk-DPair' x px) = casemk x px

DPair-rect-Type4 : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-640-v : DPair l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-DPair-v : (dpi1-v : A-v) -> (X-dpi2-v : X-f-v dpi1-v) -> Q--v (mk-DPair l11-v l10-v A-v X-f-v dpi1-v X-dpi2-v)) -> (x-640-v : DPair l11-v l10-v A-v X-f-v) -> Q--v x-640-v
DPair-rect-Type4 _ _ _ _ _ _ casemk (mk-DPair' x px) = casemk x px

DPair-rect-Type3 : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-640-v : DPair l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-DPair-v : (dpi1-v : A-v) -> (X-dpi2-v : X-f-v dpi1-v) -> Q--v (mk-DPair l11-v l10-v A-v X-f-v dpi1-v X-dpi2-v)) -> (x-640-v : DPair l11-v l10-v A-v X-f-v) -> Q--v x-640-v
DPair-rect-Type3 _ _ _ _ _ _ casemk (mk-DPair' x px) = casemk x px

DPair-rect-Type2 : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-640-v : DPair l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-DPair-v : (dpi1-v : A-v) -> (X-dpi2-v : X-f-v dpi1-v) -> Q--v (mk-DPair l11-v l10-v A-v X-f-v dpi1-v X-dpi2-v)) -> (x-640-v : DPair l11-v l10-v A-v X-f-v) -> Q--v x-640-v
DPair-rect-Type2 _ _ _ _ _ _ casemk (mk-DPair' x px) = casemk x px

DPair-rect-Type1 : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-640-v : DPair l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-DPair-v : (dpi1-v : A-v) -> (X-dpi2-v : X-f-v dpi1-v) -> Q--v (mk-DPair l11-v l10-v A-v X-f-v dpi1-v X-dpi2-v)) -> (x-640-v : DPair l11-v l10-v A-v X-f-v) -> Q--v x-640-v
DPair-rect-Type1 _ _ _ _ _ _ casemk (mk-DPair' x px) = casemk x px

DPair-rect-Type0 : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-640-v : DPair l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-DPair-v : (dpi1-v : A-v) -> (X-dpi2-v : X-f-v dpi1-v) -> Q--v (mk-DPair l11-v l10-v A-v X-f-v dpi1-v X-dpi2-v)) -> (x-640-v : DPair l11-v l10-v A-v X-f-v) -> Q--v x-640-v
DPair-rect-Type0 _ _ _ _ _ _ casemk (mk-DPair' x px) = casemk x px


dpi1 : (l2-v l1-v : Level) -> (A-v : Set l2-v) -> (f-v : (X---v : A-v) -> Set l1-v) -> (X-xxx-v : DPair l2-v l1-v A-v f-v) -> A-v
dpi1 l5-v l4-v A-v f-v X-xxx-v = match-DPair l5-v l4-v A-v f-v l5-v (λ (xxx0-v : DPair l5-v l4-v A-v f-v) -> A-v) (λ (yyy-v : A-v) -> λ (X---v : f-v yyy-v) -> yyy-v) X-xxx-v

dpi2 : (l7-v l0-v : Level) -> (A-v : Set l7-v) -> (f-v : (X---v : A-v) -> Set l0-v) -> (xxx-v : DPair l7-v l0-v A-v f-v) -> f-v (dpi1 l7-v l0-v A-v f-v xxx-v)
dpi2 l7-v l6-v A-v f-v xxx-v = match-DPair l7-v l6-v A-v f-v l6-v (λ (xxx0-v : DPair l7-v l6-v A-v f-v) -> f-v (dpi1 l7-v l6-v A-v f-v xxx0-v)) (λ (X---v : A-v) -> λ (yyy-v : f-v X---v) -> yyy-v) xxx-v



DPair-inv-ind : (l38 l36 l29 : Level) -> (x1 : Set l38) -> (x2 : (X-- : x1) -> Set l36) -> (Hterm : DPair l38 l36 x1 x2) -> (P : (X-z1104 : DPair l38 l36 x1 x2) -> Set l29) -> (X-H1 : (dpi1-v : x1) -> (X-dpi2 : x2 dpi1-v) -> (X-z1105 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P Hterm
DPair-inv-ind = λ (l38 l36 l29 : Level) -> λ (x1 : Set l38) -> λ (x2 : (X-- : x1) -> Set l36) -> λ (Hterm : DPair l38 l36 x1 x2) -> λ (P : (X-z1104 : DPair l38 l36 x1 x2) -> Set l29) -> λ (H1 : (dpi1-v : x1) -> (X-dpi2 : x2 dpi1-v) -> (X-z1105 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> DPair-ind l38 l36 ((l38 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-638 : DPair l38 l36 x1 x2) -> (X-z1105 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm X-x-638) -> P X-x-638) H1 Hterm (refl (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm)

DPair-inv-rect-Type4 : (l38 l36 l29 : Level) -> (x1 : Set l38) -> (x2 : (X-- : x1) -> Set l36) -> (Hterm : DPair l38 l36 x1 x2) -> (P : (X-z1110 : DPair l38 l36 x1 x2) -> Set l29) -> (X-H1 : (dpi1-v : x1) -> (X-dpi2 : x2 dpi1-v) -> (X-z1111 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P Hterm
DPair-inv-rect-Type4 = λ (l38 l36 l29 : Level) -> λ (x1 : Set l38) -> λ (x2 : (X-- : x1) -> Set l36) -> λ (Hterm : DPair l38 l36 x1 x2) -> λ (P : (X-z1110 : DPair l38 l36 x1 x2) -> Set l29) -> λ (H1 : (dpi1-v : x1) -> (X-dpi2 : x2 dpi1-v) -> (X-z1111 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> DPair-rect-Type4 l38 l36 ((l38 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-640 : DPair l38 l36 x1 x2) -> (X-z1111 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm X-x-640) -> P X-x-640) H1 Hterm (refl (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm)

DPair-inv-rect-Type3 : (l38 l36 l29 : Level) -> (x1 : Set l38) -> (x2 : (X-- : x1) -> Set l36) -> (Hterm : DPair l38 l36 x1 x2) -> (P : (X-z1116 : DPair l38 l36 x1 x2) -> Set l29) -> (X-H1 : (dpi1-v : x1) -> (X-dpi2 : x2 dpi1-v) -> (X-z1117 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P Hterm
DPair-inv-rect-Type3 = λ (l38 l36 l29 : Level) -> λ (x1 : Set l38) -> λ (x2 : (X-- : x1) -> Set l36) -> λ (Hterm : DPair l38 l36 x1 x2) -> λ (P : (X-z1116 : DPair l38 l36 x1 x2) -> Set l29) -> λ (H1 : (dpi1-v : x1) -> (X-dpi2 : x2 dpi1-v) -> (X-z1117 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> DPair-rect-Type3 l38 l36 ((l38 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-644 : DPair l38 l36 x1 x2) -> (X-z1117 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm X-x-644) -> P X-x-644) H1 Hterm (refl (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm)

DPair-inv-rect-Type2 : (l38 l36 l29 : Level) -> (x1 : Set l38) -> (x2 : (X-- : x1) -> Set l36) -> (Hterm : DPair l38 l36 x1 x2) -> (P : (X-z1122 : DPair l38 l36 x1 x2) -> Set l29) -> (X-H1 : (dpi1-v : x1) -> (X-dpi2 : x2 dpi1-v) -> (X-z1123 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P Hterm
DPair-inv-rect-Type2 = λ (l38 l36 l29 : Level) -> λ (x1 : Set l38) -> λ (x2 : (X-- : x1) -> Set l36) -> λ (Hterm : DPair l38 l36 x1 x2) -> λ (P : (X-z1122 : DPair l38 l36 x1 x2) -> Set l29) -> λ (H1 : (dpi1-v : x1) -> (X-dpi2 : x2 dpi1-v) -> (X-z1123 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> DPair-rect-Type2 l38 l36 ((l38 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-646 : DPair l38 l36 x1 x2) -> (X-z1123 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm X-x-646) -> P X-x-646) H1 Hterm (refl (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm)

DPair-inv-rect-Type1 : (l38 l36 l29 : Level) -> (x1 : Set l38) -> (x2 : (X-- : x1) -> Set l36) -> (Hterm : DPair l38 l36 x1 x2) -> (P : (X-z1128 : DPair l38 l36 x1 x2) -> Set l29) -> (X-H1 : (dpi1-v : x1) -> (X-dpi2 : x2 dpi1-v) -> (X-z1129 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P Hterm
DPair-inv-rect-Type1 = λ (l38 l36 l29 : Level) -> λ (x1 : Set l38) -> λ (x2 : (X-- : x1) -> Set l36) -> λ (Hterm : DPair l38 l36 x1 x2) -> λ (P : (X-z1128 : DPair l38 l36 x1 x2) -> Set l29) -> λ (H1 : (dpi1-v : x1) -> (X-dpi2 : x2 dpi1-v) -> (X-z1129 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> DPair-rect-Type1 l38 l36 ((l38 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-648 : DPair l38 l36 x1 x2) -> (X-z1129 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm X-x-648) -> P X-x-648) H1 Hterm (refl (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm)

DPair-inv-rect-Type0 : (l38 l36 l29 : Level) -> (x1 : Set l38) -> (x2 : (X-- : x1) -> Set l36) -> (Hterm : DPair l38 l36 x1 x2) -> (P : (X-z1134 : DPair l38 l36 x1 x2) -> Set l29) -> (X-H1 : (dpi1-v : x1) -> (X-dpi2 : x2 dpi1-v) -> (X-z1135 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P Hterm
DPair-inv-rect-Type0 = λ (l38 l36 l29 : Level) -> λ (x1 : Set l38) -> λ (x2 : (X-- : x1) -> Set l36) -> λ (Hterm : DPair l38 l36 x1 x2) -> λ (P : (X-z1134 : DPair l38 l36 x1 x2) -> Set l29) -> λ (H1 : (dpi1-v : x1) -> (X-dpi2 : x2 dpi1-v) -> (X-z1135 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> P (mk-DPair l38 l36 x1 x2 dpi1-v X-dpi2)) -> DPair-rect-Type0 l38 l36 ((l38 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-650 : DPair l38 l36 x1 x2) -> (X-z1135 : eq (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm X-x-650) -> P X-x-650) H1 Hterm (refl (l38 ⊔ l36) (DPair l38 l36 x1 x2) Hterm)

DPair-discr : (l172 l171 l217 : Level) -> (a1 : Set l172) -> (a2 : (X-- : a1) -> Set l171) -> (x : DPair l172 l171 a1 a2) -> (y : DPair l172 l171 a1 a2) -> (X-e : eq (l172 ⊔ l171) (DPair l172 l171 a1 a2) x y) -> match-DPair l172 l171 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc l171) ⊔ (lsuc l172)) ⊔ (lsuc (lsuc l217)))) (λ (X-- : DPair l172 l171 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171))) (λ (t0 : a1) -> λ (t1 : a2 t0) -> match-DPair l172 l171 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l217)) ⊔ (lsuc l172)) ⊔ (lsuc l171))) (λ (X-- : DPair l172 l171 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171))) (λ (u0 : a1) -> λ (u1 : a2 u0) -> (P : Set l217) -> (X-z41 : (e0 : eq l172 a1 (R0 l172 a1 t0) u0) -> (X-e1 : eq l171 (a2 u0) (R1 l172 l171 a1 t0 (λ (x0 : a1) -> λ (p0 : eq l172 a1 t0 x0) -> a2 x0) t1 u0 e0) u1) -> P) -> P) y) x
DPair-discr = λ (l172 l171 l217 : Level) -> λ (a1 : Set l172) -> λ (a2 : (X-- : a1) -> Set l171) -> λ (x : DPair l172 l171 a1 a2) -> λ (y : DPair l172 l171 a1 a2) -> λ (Deq : eq (l172 ⊔ l171) (DPair l172 l171 a1 a2) x y) -> eq-rect-Type2 (l172 ⊔ l171) ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171)) (DPair l172 l171 a1 a2) x (λ (x-13 : DPair l172 l171 a1 a2) -> λ (X-x-14 : eq (l172 ⊔ l171) (DPair l172 l171 a1 a2) x x-13) -> match-DPair l172 l171 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l217)) ⊔ (lsuc l172)) ⊔ (lsuc l171))) (λ (X-- : DPair l172 l171 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171))) (λ (t0 : a1) -> λ (t1 : a2 t0) -> match-DPair l172 l171 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l217)) ⊔ (lsuc l172)) ⊔ (lsuc l171))) (λ (X-- : DPair l172 l171 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171))) (λ (u0 : a1) -> λ (u1 : a2 u0) -> (P : Set l217) -> (X-z41 : (e0 : eq l172 a1 (R0 l172 a1 t0) u0) -> (X-e1 : eq l171 (a2 u0) (R1 l172 l171 a1 t0 (λ (x0 : a1) -> λ (p0 : eq l172 a1 t0 x0) -> a2 x0) t1 u0 e0) u1) -> P) -> P) x-13) x) (match-DPair l172 l171 a1 a2 ((lsuc lzero) ⊔ ((l171 ⊔ l172) ⊔ (lsuc l217))) (λ (X-- : DPair l172 l171 a1 a2) -> match-DPair l172 l171 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l217)) ⊔ (lsuc l172)) ⊔ (lsuc l171))) (λ (X-0 : DPair l172 l171 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171))) (λ (t0 : a1) -> λ (t1 : a2 t0) -> match-DPair l172 l171 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l217)) ⊔ (lsuc l172)) ⊔ (lsuc l171))) (λ (X-0 : DPair l172 l171 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171))) (λ (u0 : a1) -> λ (u1 : a2 u0) -> (P : Set l217) -> (X-z41 : (e0 : eq l172 a1 (R0 l172 a1 t0) u0) -> (X-e1 : eq l171 (a2 u0) (R1 l172 l171 a1 t0 (λ (x0 : a1) -> λ (p0 : eq l172 a1 t0 x0) -> a2 x0) t1 u0 e0) u1) -> P) -> P) X--) X--) (λ (a0 : a1) -> λ (a10 : a2 a0) -> λ (P : Set l217) -> λ (DH : (e0 : eq l172 a1 (R0 l172 a1 a0) a0) -> (X-e1 : eq l171 (a2 a0) (R1 l172 l171 a1 a0 (λ (x0 : a1) -> λ (p0 : eq l172 a1 a0 x0) -> a2 x0) a10 a0 e0) a10) -> P) -> DH (refl l172 a1 (R0 l172 a1 a0)) (refl l171 (a2 a0) (R1 l172 l171 a1 a0 (λ (x0 : a1) -> λ (p0 : eq l172 a1 a0 x0) -> a2 x0) a10 a0 (refl l172 a1 (R0 l172 a1 a0))))) x) y Deq

data Sig (l2-v l1-v : Level) (A-v : Set l2-v)  (f-v : (X---v : A-v) -> Set l1-v) : Set (lzero ⊔ (l2-v ⊔ l1-v)) where
  mk-Sig' : (pi1-v : A-v) -> (X-pi2-v : f-v pi1-v) -> Sig l2-v l1-v A-v f-v

mk-Sig : (l1-v l3-v : Level) -> (A-v : Set l1-v) -> (f-v : (X---v : A-v) -> Set l3-v) -> (pi1-v : A-v) -> (X-pi2-v : f-v pi1-v) -> Sig l1-v l3-v A-v f-v
mk-Sig _ _ _ _ = mk-Sig'

match-Sig : (l8-v l7-v : Level) -> (A-v : Set l8-v) -> (X-f-v : (X---v : A-v) -> Set l7-v) -> (return-sort-v : Level) -> (return-type-v : (z-v : Sig l8-v l7-v A-v X-f-v) -> Set return-sort-v) -> (case-mk-Sig-v : (pi1-v : A-v) -> (X-pi2-v : X-f-v pi1-v) -> return-type-v (mk-Sig l8-v l7-v A-v X-f-v pi1-v X-pi2-v)) -> (z-v : Sig l8-v l7-v A-v X-f-v) -> return-type-v z-v
match-Sig _ _ _ _ _ _ casemk (mk-Sig' x y) = casemk x y

Sig-ind : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-664-v : Sig l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-Sig-v : (pi1-v : A-v) -> (X-pi2-v : X-f-v pi1-v) -> Q--v (mk-Sig l11-v l10-v A-v X-f-v pi1-v X-pi2-v)) -> (x-664-v : Sig l11-v l10-v A-v X-f-v) -> Q--v x-664-v
Sig-ind _ _ _ _ _ _ casemk (mk-Sig' x y) = casemk x y

Sig-rect-Type5 : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-666-v : Sig l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-Sig-v : (pi1-v : A-v) -> (X-pi2-v : X-f-v pi1-v) -> Q--v (mk-Sig l11-v l10-v A-v X-f-v pi1-v X-pi2-v)) -> (x-666-v : Sig l11-v l10-v A-v X-f-v) -> Q--v x-666-v
Sig-rect-Type5 _ _ _ _ _ _ casemk (mk-Sig' x y) = casemk x y

Sig-rect-Type4 : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-666-v : Sig l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-Sig-v : (pi1-v : A-v) -> (X-pi2-v : X-f-v pi1-v) -> Q--v (mk-Sig l11-v l10-v A-v X-f-v pi1-v X-pi2-v)) -> (x-666-v : Sig l11-v l10-v A-v X-f-v) -> Q--v x-666-v
Sig-rect-Type4 _ _ _ _ _ _ casemk (mk-Sig' x y) = casemk x y

Sig-rect-Type3 : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-666-v : Sig l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-Sig-v : (pi1-v : A-v) -> (X-pi2-v : X-f-v pi1-v) -> Q--v (mk-Sig l11-v l10-v A-v X-f-v pi1-v X-pi2-v)) -> (x-666-v : Sig l11-v l10-v A-v X-f-v) -> Q--v x-666-v
Sig-rect-Type3 _ _ _ _ _ _ casemk (mk-Sig' x y) = casemk x y

Sig-rect-Type2 : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-666-v : Sig l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-Sig-v : (pi1-v : A-v) -> (X-pi2-v : X-f-v pi1-v) -> Q--v (mk-Sig l11-v l10-v A-v X-f-v pi1-v X-pi2-v)) -> (x-666-v : Sig l11-v l10-v A-v X-f-v) -> Q--v x-666-v
Sig-rect-Type2 _ _ _ _ _ _ casemk (mk-Sig' x y) = casemk x y

Sig-rect-Type1 : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-666-v : Sig l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-Sig-v : (pi1-v : A-v) -> (X-pi2-v : X-f-v pi1-v) -> Q--v (mk-Sig l11-v l10-v A-v X-f-v pi1-v X-pi2-v)) -> (x-666-v : Sig l11-v l10-v A-v X-f-v) -> Q--v x-666-v
Sig-rect-Type1 _ _ _ _ _ _ casemk (mk-Sig' x y) = casemk x y

Sig-rect-Type0 : (l11-v l10-v l6-v : Level) -> (A-v : Set l11-v) -> (X-f-v : (X---v : A-v) -> Set l10-v) -> (Q--v : (X-x-666-v : Sig l11-v l10-v A-v X-f-v) -> Set l6-v) -> (X-H-mk-Sig-v : (pi1-v : A-v) -> (X-pi2-v : X-f-v pi1-v) -> Q--v (mk-Sig l11-v l10-v A-v X-f-v pi1-v X-pi2-v)) -> (x-666-v : Sig l11-v l10-v A-v X-f-v) -> Q--v x-666-v
Sig-rect-Type0 _ _ _ _ _ _ casemk (mk-Sig' x y) = casemk x y

pi1 : (l2-v l1-v : Level) -> (A-v : Set l2-v) -> (f-v : (X---v : A-v) -> Set l1-v) -> (X-xxx-v : Sig l2-v l1-v A-v f-v) -> A-v
pi1 l5-v l4-v A-v f-v X-xxx-v = match-Sig l5-v l4-v A-v f-v l5-v (λ (xxx0-v : Sig l5-v l4-v A-v f-v) -> A-v) (λ (yyy-v : A-v) -> λ (X---v : f-v yyy-v) -> yyy-v) X-xxx-v

pi2 : (l7-v l0-v : Level) -> (A-v : Set l7-v) -> (f-v : (X---v : A-v) -> Set l0-v) -> (xxx-v : Sig l7-v l0-v A-v f-v) -> f-v (pi1 l7-v l0-v A-v f-v xxx-v)
pi2 l7-v l6-v A-v f-v xxx-v = match-Sig l7-v l6-v A-v f-v l6-v (λ (xxx0-v : Sig l7-v l6-v A-v f-v) -> f-v (pi1 l7-v l6-v A-v f-v xxx0-v)) (λ (X---v : A-v) -> λ (yyy-v : f-v X---v) -> yyy-v) xxx-v


Sig-inv-ind : (l38 l36 l29 : Level) -> (x1 : Set l38) -> (x2 : (X-- : x1) -> Set l36) -> (Hterm : Sig l38 l36 x1 x2) -> (P : (X-z1170 : Sig l38 l36 x1 x2) -> Set l29) -> (X-H1 : (pi1-v : x1) -> (X-pi2 : x2 pi1-v) -> (X-z1171 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P Hterm
Sig-inv-ind = λ (l38 l36 l29 : Level) -> λ (x1 : Set l38) -> λ (x2 : (X-- : x1) -> Set l36) -> λ (Hterm : Sig l38 l36 x1 x2) -> λ (P : (X-z1170 : Sig l38 l36 x1 x2) -> Set l29) -> λ (H1 : (pi1-v : x1) -> (X-pi2 : x2 pi1-v) -> (X-z1171 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> Sig-ind l38 l36 ((l38 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-664 : Sig l38 l36 x1 x2) -> (X-z1171 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm X-x-664) -> P X-x-664) H1 Hterm (refl (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm)

Sig-inv-rect-Type4 : (l38 l36 l29 : Level) -> (x1 : Set l38) -> (x2 : (X-- : x1) -> Set l36) -> (Hterm : Sig l38 l36 x1 x2) -> (P : (X-z1176 : Sig l38 l36 x1 x2) -> Set l29) -> (X-H1 : (pi1-v : x1) -> (X-pi2 : x2 pi1-v) -> (X-z1177 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P Hterm
Sig-inv-rect-Type4 = λ (l38 l36 l29 : Level) -> λ (x1 : Set l38) -> λ (x2 : (X-- : x1) -> Set l36) -> λ (Hterm : Sig l38 l36 x1 x2) -> λ (P : (X-z1176 : Sig l38 l36 x1 x2) -> Set l29) -> λ (H1 : (pi1-v : x1) -> (X-pi2 : x2 pi1-v) -> (X-z1177 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> Sig-rect-Type4 l38 l36 ((l38 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-666 : Sig l38 l36 x1 x2) -> (X-z1177 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm X-x-666) -> P X-x-666) H1 Hterm (refl (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm)

Sig-inv-rect-Type3 : (l38 l36 l29 : Level) -> (x1 : Set l38) -> (x2 : (X-- : x1) -> Set l36) -> (Hterm : Sig l38 l36 x1 x2) -> (P : (X-z1182 : Sig l38 l36 x1 x2) -> Set l29) -> (X-H1 : (pi1-v : x1) -> (X-pi2 : x2 pi1-v) -> (X-z1183 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P Hterm
Sig-inv-rect-Type3 = λ (l38 l36 l29 : Level) -> λ (x1 : Set l38) -> λ (x2 : (X-- : x1) -> Set l36) -> λ (Hterm : Sig l38 l36 x1 x2) -> λ (P : (X-z1182 : Sig l38 l36 x1 x2) -> Set l29) -> λ (H1 : (pi1-v : x1) -> (X-pi2 : x2 pi1-v) -> (X-z1183 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> Sig-rect-Type3 l38 l36 ((l38 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-670 : Sig l38 l36 x1 x2) -> (X-z1183 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm X-x-670) -> P X-x-670) H1 Hterm (refl (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm)

Sig-inv-rect-Type2 : (l38 l36 l29 : Level) -> (x1 : Set l38) -> (x2 : (X-- : x1) -> Set l36) -> (Hterm : Sig l38 l36 x1 x2) -> (P : (X-z1188 : Sig l38 l36 x1 x2) -> Set l29) -> (X-H1 : (pi1-v : x1) -> (X-pi2 : x2 pi1-v) -> (X-z1189 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P Hterm
Sig-inv-rect-Type2 = λ (l38 l36 l29 : Level) -> λ (x1 : Set l38) -> λ (x2 : (X-- : x1) -> Set l36) -> λ (Hterm : Sig l38 l36 x1 x2) -> λ (P : (X-z1188 : Sig l38 l36 x1 x2) -> Set l29) -> λ (H1 : (pi1-v : x1) -> (X-pi2 : x2 pi1-v) -> (X-z1189 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> Sig-rect-Type2 l38 l36 ((l38 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-672 : Sig l38 l36 x1 x2) -> (X-z1189 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm X-x-672) -> P X-x-672) H1 Hterm (refl (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm)

Sig-inv-rect-Type1 : (l38 l36 l29 : Level) -> (x1 : Set l38) -> (x2 : (X-- : x1) -> Set l36) -> (Hterm : Sig l38 l36 x1 x2) -> (P : (X-z1194 : Sig l38 l36 x1 x2) -> Set l29) -> (X-H1 : (pi1-v : x1) -> (X-pi2 : x2 pi1-v) -> (X-z1195 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P Hterm
Sig-inv-rect-Type1 = λ (l38 l36 l29 : Level) -> λ (x1 : Set l38) -> λ (x2 : (X-- : x1) -> Set l36) -> λ (Hterm : Sig l38 l36 x1 x2) -> λ (P : (X-z1194 : Sig l38 l36 x1 x2) -> Set l29) -> λ (H1 : (pi1-v : x1) -> (X-pi2 : x2 pi1-v) -> (X-z1195 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> Sig-rect-Type1 l38 l36 ((l38 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-674 : Sig l38 l36 x1 x2) -> (X-z1195 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm X-x-674) -> P X-x-674) H1 Hterm (refl (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm)

Sig-inv-rect-Type0 : (l38 l36 l29 : Level) -> (x1 : Set l38) -> (x2 : (X-- : x1) -> Set l36) -> (Hterm : Sig l38 l36 x1 x2) -> (P : (X-z1200 : Sig l38 l36 x1 x2) -> Set l29) -> (X-H1 : (pi1-v : x1) -> (X-pi2 : x2 pi1-v) -> (X-z1201 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P Hterm
Sig-inv-rect-Type0 = λ (l38 l36 l29 : Level) -> λ (x1 : Set l38) -> λ (x2 : (X-- : x1) -> Set l36) -> λ (Hterm : Sig l38 l36 x1 x2) -> λ (P : (X-z1200 : Sig l38 l36 x1 x2) -> Set l29) -> λ (H1 : (pi1-v : x1) -> (X-pi2 : x2 pi1-v) -> (X-z1201 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> P (mk-Sig l38 l36 x1 x2 pi1-v X-pi2)) -> Sig-rect-Type0 l38 l36 ((l38 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-676 : Sig l38 l36 x1 x2) -> (X-z1201 : eq (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm X-x-676) -> P X-x-676) H1 Hterm (refl (l38 ⊔ l36) (Sig l38 l36 x1 x2) Hterm)

Sig-discr : (l172 l171 l217 : Level) -> (a1 : Set l172) -> (a2 : (X-- : a1) -> Set l171) -> (x : Sig l172 l171 a1 a2) -> (y : Sig l172 l171 a1 a2) -> (X-e : eq (l172 ⊔ l171) (Sig l172 l171 a1 a2) x y) -> match-Sig l172 l171 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc l171) ⊔ (lsuc l172)) ⊔ (lsuc (lsuc l217)))) (λ (X-- : Sig l172 l171 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171))) (λ (t0 : a1) -> λ (t1 : a2 t0) -> match-Sig l172 l171 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l217)) ⊔ (lsuc l172)) ⊔ (lsuc l171))) (λ (X-- : Sig l172 l171 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171))) (λ (u0 : a1) -> λ (u1 : a2 u0) -> (P : Set l217) -> (X-z43 : (e0 : eq l172 a1 (R0 l172 a1 t0) u0) -> (X-e1 : eq l171 (a2 u0) (R1 l172 l171 a1 t0 (λ (x-19 : a1) -> λ (X-x-20 : eq l172 a1 t0 x-19) -> a2 x-19) t1 u0 e0) u1) -> P) -> P) y) x
Sig-discr = λ (l172 l171 l217 : Level) -> λ (a1 : Set l172) -> λ (a2 : (X-- : a1) -> Set l171) -> λ (x : Sig l172 l171 a1 a2) -> λ (y : Sig l172 l171 a1 a2) -> λ (Deq : eq (l172 ⊔ l171) (Sig l172 l171 a1 a2) x y) -> eq-rect-Type2 (l172 ⊔ l171) ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171)) (Sig l172 l171 a1 a2) x (λ (x-13 : Sig l172 l171 a1 a2) -> λ (X-x-14 : eq (l172 ⊔ l171) (Sig l172 l171 a1 a2) x x-13) -> match-Sig l172 l171 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l217)) ⊔ (lsuc l172)) ⊔ (lsuc l171))) (λ (X-- : Sig l172 l171 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171))) (λ (t0 : a1) -> λ (t1 : a2 t0) -> match-Sig l172 l171 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l217)) ⊔ (lsuc l172)) ⊔ (lsuc l171))) (λ (X-- : Sig l172 l171 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171))) (λ (u0 : a1) -> λ (u1 : a2 u0) -> (P : Set l217) -> (X-z43 : (e0 : eq l172 a1 (R0 l172 a1 t0) u0) -> (X-e1 : eq l171 (a2 u0) (R1 l172 l171 a1 t0 (λ (x-19 : a1) -> λ (X-x-20 : eq l172 a1 t0 x-19) -> a2 x-19) t1 u0 e0) u1) -> P) -> P) x-13) x) (match-Sig l172 l171 a1 a2 ((lsuc lzero) ⊔ ((l171 ⊔ l172) ⊔ (lsuc l217))) (λ (X-- : Sig l172 l171 a1 a2) -> match-Sig l172 l171 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l217)) ⊔ (lsuc l172)) ⊔ (lsuc l171))) (λ (X-0 : Sig l172 l171 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171))) (λ (t0 : a1) -> λ (t1 : a2 t0) -> match-Sig l172 l171 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l217)) ⊔ (lsuc l172)) ⊔ (lsuc l171))) (λ (X-0 : Sig l172 l171 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l217) ⊔ l172) ⊔ l171))) (λ (u0 : a1) -> λ (u1 : a2 u0) -> (P : Set l217) -> (X-z43 : (e0 : eq l172 a1 (R0 l172 a1 t0) u0) -> (X-e1 : eq l171 (a2 u0) (R1 l172 l171 a1 t0 (λ (x-19 : a1) -> λ (X-x-20 : eq l172 a1 t0 x-19) -> a2 x-19) t1 u0 e0) u1) -> P) -> P) X--) X--) (λ (a0 : a1) -> λ (a10 : a2 a0) -> λ (P : Set l217) -> λ (DH : (e0 : eq l172 a1 (R0 l172 a1 a0) a0) -> (X-e1 : eq l171 (a2 a0) (R1 l172 l171 a1 a0 (λ (x-19 : a1) -> λ (X-x-20 : eq l172 a1 a0 x-19) -> a2 x-19) a10 a0 e0) a10) -> P) -> DH (refl l172 a1 (R0 l172 a1 a0)) (refl l171 (a2 a0) (R1 l172 l171 a1 a0 (λ (x-19 : a1) -> λ (X-x-20 : eq l172 a1 a0 x-19) -> a2 x-19) a10 a0 (refl l172 a1 (R0 l172 a1 a0))))) x) y Deq

sub-pi2 : (l30 l22 l20 : Level) -> (A : Set l30) -> (P : (X-- : A) -> Set l22) -> (P' : (X-- : A) -> Set l20) -> (X-- : (x : A) -> (X-- : P x) -> P' x) -> (x : Sig l30 l22 A (λ (x : A) -> P x)) -> P' (pi1 l30 l22 A (λ (x0 : A) -> P x0) x)
sub-pi2 = λ (l30 l22 l20 : Level) -> λ (A : Set l30) -> λ (P : (X-- : A) -> Set l22) -> λ (P' : (X-- : A) -> Set l20) -> λ (H1 : (x : A) -> (X-- : P x) -> P' x) -> λ (X-clearme : Sig l30 l22 A (λ (x : A) -> P x)) -> match-Sig l30 l22 A (λ (x : A) -> P x) l20 (λ (X-- : Sig l30 l22 A (λ (x : A) -> P x)) -> P' (pi1 l30 l22 A (λ (x0 : A) -> P x0) X--)) (λ (x : A) -> λ (H2 : P x) -> H1 x H2) X-clearme

inj-mk-Sig : (l27 l25 : Level) -> (A : Set l27) -> (P : (X-- : A) -> Set l25) -> (x : Sig l27 l25 A P) -> eq (l27 ⊔ l25) (Sig l27 l25 A P) x (mk-Sig l27 l25 A P (pi1 l27 l25 A P x) (pi2 l27 l25 A P x))
inj-mk-Sig = λ (l27 l25 : Level) -> λ (A : Set l27) -> λ (P : (X-- : A) -> Set l25) -> λ (x : Sig l27 l25 A P) -> match-Sig l27 l25 A P (l27 ⊔ l25) (λ (X-- : Sig l27 l25 A P) -> eq (l27 ⊔ l25) (Sig l27 l25 A P) X-- (mk-Sig l27 l25 A P (pi1 l27 l25 A P X--) (pi2 l27 l25 A P X--))) (λ (pi1-v : A) -> λ (X-pi2 : P pi1-v) -> refl (l27 ⊔ l25) (Sig l27 l25 A P) (mk-Sig l27 l25 A P pi1-v X-pi2)) x


data Prod (l2-v l1-v : Level)  (A-v : Set l2-v)  (B-v : Set l1-v) : Set (lzero ⊔ (l2-v ⊔ l1-v)) where
  mk-Prod' : (X-fst-v : A-v) -> (X-snd-v : B-v) -> Prod l2-v l1-v A-v B-v

mk-Prod : (l4-v l3-v : Level) -> (A-v : Set l4-v) -> (B-v : Set l3-v) -> (X-fst-v : A-v) -> (X-snd-v : B-v) -> Prod l4-v l3-v A-v B-v
mk-Prod _ _ _ _ = mk-Prod'

match-Prod : (l8-v l7-v : Level) -> (X-A-v : Set l8-v) -> (X-B-v : Set l7-v) -> (return-sort-v : Level) -> (return-type-v : (z-v : Prod l8-v l7-v X-A-v X-B-v) -> Set return-sort-v) -> (case-mk-Prod-v : (X-fst-v : X-A-v) -> (X-snd-v : X-B-v) -> return-type-v (mk-Prod l8-v l7-v X-A-v X-B-v X-fst-v X-snd-v)) -> (z-v : Prod l8-v l7-v X-A-v X-B-v) -> return-type-v z-v
match-Prod _ _ _ _ _ _ casemk (mk-Prod' x y) = casemk x y

Prod-ind : (l11-v l10-v l6-v : Level) -> (X-A-v : Set l11-v) -> (X-B-v : Set l10-v) -> (Q--v : (X-x-690-v : Prod l11-v l10-v X-A-v X-B-v) -> Set l6-v) -> (X-H-mk-Prod-v : (X-fst-v : X-A-v) -> (X-snd-v : X-B-v) -> Q--v (mk-Prod l11-v l10-v X-A-v X-B-v X-fst-v X-snd-v)) -> (x-690-v : Prod l11-v l10-v X-A-v X-B-v) -> Q--v x-690-v
Prod-ind _ _ _ _ _ _ casemk (mk-Prod' x y) = casemk x y

Prod-rect-Type5 : (l11-v l10-v l6-v : Level) -> (X-A-v : Set l11-v) -> (X-B-v : Set l10-v) -> (Q--v : (X-x-692-v : Prod l11-v l10-v X-A-v X-B-v) -> Set l6-v) -> (X-H-mk-Prod-v : (X-fst-v : X-A-v) -> (X-snd-v : X-B-v) -> Q--v (mk-Prod l11-v l10-v X-A-v X-B-v X-fst-v X-snd-v)) -> (x-692-v : Prod l11-v l10-v X-A-v X-B-v) -> Q--v x-692-v
Prod-rect-Type5 _ _ _ _ _ _ casemk (mk-Prod' x y) = casemk x y

Prod-rect-Type4 : (l11-v l10-v l6-v : Level) -> (X-A-v : Set l11-v) -> (X-B-v : Set l10-v) -> (Q--v : (X-x-692-v : Prod l11-v l10-v X-A-v X-B-v) -> Set l6-v) -> (X-H-mk-Prod-v : (X-fst-v : X-A-v) -> (X-snd-v : X-B-v) -> Q--v (mk-Prod l11-v l10-v X-A-v X-B-v X-fst-v X-snd-v)) -> (x-692-v : Prod l11-v l10-v X-A-v X-B-v) -> Q--v x-692-v
Prod-rect-Type4 _ _ _ _ _ _ casemk (mk-Prod' x y) = casemk x y

Prod-rect-Type3 : (l11-v l10-v l6-v : Level) -> (X-A-v : Set l11-v) -> (X-B-v : Set l10-v) -> (Q--v : (X-x-692-v : Prod l11-v l10-v X-A-v X-B-v) -> Set l6-v) -> (X-H-mk-Prod-v : (X-fst-v : X-A-v) -> (X-snd-v : X-B-v) -> Q--v (mk-Prod l11-v l10-v X-A-v X-B-v X-fst-v X-snd-v)) -> (x-692-v : Prod l11-v l10-v X-A-v X-B-v) -> Q--v x-692-v
Prod-rect-Type3 _ _ _ _ _ _ casemk (mk-Prod' x y) = casemk x y

Prod-rect-Type2 : (l11-v l10-v l6-v : Level) -> (X-A-v : Set l11-v) -> (X-B-v : Set l10-v) -> (Q--v : (X-x-692-v : Prod l11-v l10-v X-A-v X-B-v) -> Set l6-v) -> (X-H-mk-Prod-v : (X-fst-v : X-A-v) -> (X-snd-v : X-B-v) -> Q--v (mk-Prod l11-v l10-v X-A-v X-B-v X-fst-v X-snd-v)) -> (x-692-v : Prod l11-v l10-v X-A-v X-B-v) -> Q--v x-692-v
Prod-rect-Type2 _ _ _ _ _ _ casemk (mk-Prod' x y) = casemk x y

Prod-rect-Type1 : (l11-v l10-v l6-v : Level) -> (X-A-v : Set l11-v) -> (X-B-v : Set l10-v) -> (Q--v : (X-x-692-v : Prod l11-v l10-v X-A-v X-B-v) -> Set l6-v) -> (X-H-mk-Prod-v : (X-fst-v : X-A-v) -> (X-snd-v : X-B-v) -> Q--v (mk-Prod l11-v l10-v X-A-v X-B-v X-fst-v X-snd-v)) -> (x-692-v : Prod l11-v l10-v X-A-v X-B-v) -> Q--v x-692-v
Prod-rect-Type1 _ _ _ _ _ _ casemk (mk-Prod' x y) = casemk x y

Prod-rect-Type0 : (l11-v l10-v l6-v : Level) -> (X-A-v : Set l11-v) -> (X-B-v : Set l10-v) -> (Q--v : (X-x-692-v : Prod l11-v l10-v X-A-v X-B-v) -> Set l6-v) -> (X-H-mk-Prod-v : (X-fst-v : X-A-v) -> (X-snd-v : X-B-v) -> Q--v (mk-Prod l11-v l10-v X-A-v X-B-v X-fst-v X-snd-v)) -> (x-692-v : Prod l11-v l10-v X-A-v X-B-v) -> Q--v x-692-v
Prod-rect-Type0 _ _ _ _ _ _ casemk (mk-Prod' x y) = casemk x y


fst : (l2-v l1-v : Level) -> (A-v : Set l2-v) -> (B-v : Set l1-v) -> (X-xxx-v : Prod l2-v l1-v A-v B-v) -> A-v
fst l5-v l4-v A-v B-v X-xxx-v = match-Prod l5-v l4-v A-v B-v l5-v (λ (xxx0-v : Prod l5-v l4-v A-v B-v) -> A-v) (λ (yyy-v : A-v) -> λ (X---v : B-v) -> yyy-v) X-xxx-v

snd : (l2-v l1-v : Level) -> (A-v : Set l2-v) -> (B-v : Set l1-v) -> (X-xxx-v : Prod l2-v l1-v A-v B-v) -> B-v
snd l5-v l4-v A-v B-v X-xxx-v = match-Prod l5-v l4-v A-v B-v l4-v (λ (xxx0-v : Prod l5-v l4-v A-v B-v) -> B-v) (λ (X---v : A-v) -> λ (yyy-v : B-v) -> yyy-v) X-xxx-v



Prod-inv-ind : (l37 l36 l29 : Level) -> (x1 : Set l37) -> (x2 : Set l36) -> (Hterm : Prod l37 l36 x1 x2) -> (P : (X-z1236 : Prod l37 l36 x1 x2) -> Set l29) -> (X-H1 : (X-fst : x1) -> (X-snd : x2) -> (X-z1237 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P Hterm
Prod-inv-ind = λ (l37 l36 l29 : Level) -> λ (x1 : Set l37) -> λ (x2 : Set l36) -> λ (Hterm : Prod l37 l36 x1 x2) -> λ (P : (X-z1236 : Prod l37 l36 x1 x2) -> Set l29) -> λ (H1 : (X-fst : x1) -> (X-snd : x2) -> (X-z1237 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> Prod-ind l37 l36 ((l37 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-690 : Prod l37 l36 x1 x2) -> (X-z1237 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm X-x-690) -> P X-x-690) H1 Hterm (refl (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm)

Prod-inv-rect-Type4 : (l37 l36 l29 : Level) -> (x1 : Set l37) -> (x2 : Set l36) -> (Hterm : Prod l37 l36 x1 x2) -> (P : (X-z1242 : Prod l37 l36 x1 x2) -> Set l29) -> (X-H1 : (X-fst : x1) -> (X-snd : x2) -> (X-z1243 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P Hterm
Prod-inv-rect-Type4 = λ (l37 l36 l29 : Level) -> λ (x1 : Set l37) -> λ (x2 : Set l36) -> λ (Hterm : Prod l37 l36 x1 x2) -> λ (P : (X-z1242 : Prod l37 l36 x1 x2) -> Set l29) -> λ (H1 : (X-fst : x1) -> (X-snd : x2) -> (X-z1243 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> Prod-rect-Type4 l37 l36 ((l37 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-692 : Prod l37 l36 x1 x2) -> (X-z1243 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm X-x-692) -> P X-x-692) H1 Hterm (refl (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm)

Prod-inv-rect-Type3 : (l37 l36 l29 : Level) -> (x1 : Set l37) -> (x2 : Set l36) -> (Hterm : Prod l37 l36 x1 x2) -> (P : (X-z1248 : Prod l37 l36 x1 x2) -> Set l29) -> (X-H1 : (X-fst : x1) -> (X-snd : x2) -> (X-z1249 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P Hterm
Prod-inv-rect-Type3 = λ (l37 l36 l29 : Level) -> λ (x1 : Set l37) -> λ (x2 : Set l36) -> λ (Hterm : Prod l37 l36 x1 x2) -> λ (P : (X-z1248 : Prod l37 l36 x1 x2) -> Set l29) -> λ (H1 : (X-fst : x1) -> (X-snd : x2) -> (X-z1249 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> Prod-rect-Type3 l37 l36 ((l37 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-696 : Prod l37 l36 x1 x2) -> (X-z1249 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm X-x-696) -> P X-x-696) H1 Hterm (refl (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm)

Prod-inv-rect-Type2 : (l37 l36 l29 : Level) -> (x1 : Set l37) -> (x2 : Set l36) -> (Hterm : Prod l37 l36 x1 x2) -> (P : (X-z1254 : Prod l37 l36 x1 x2) -> Set l29) -> (X-H1 : (X-fst : x1) -> (X-snd : x2) -> (X-z1255 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P Hterm
Prod-inv-rect-Type2 = λ (l37 l36 l29 : Level) -> λ (x1 : Set l37) -> λ (x2 : Set l36) -> λ (Hterm : Prod l37 l36 x1 x2) -> λ (P : (X-z1254 : Prod l37 l36 x1 x2) -> Set l29) -> λ (H1 : (X-fst : x1) -> (X-snd : x2) -> (X-z1255 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> Prod-rect-Type2 l37 l36 ((l37 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-698 : Prod l37 l36 x1 x2) -> (X-z1255 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm X-x-698) -> P X-x-698) H1 Hterm (refl (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm)

Prod-inv-rect-Type1 : (l37 l36 l29 : Level) -> (x1 : Set l37) -> (x2 : Set l36) -> (Hterm : Prod l37 l36 x1 x2) -> (P : (X-z1260 : Prod l37 l36 x1 x2) -> Set l29) -> (X-H1 : (X-fst : x1) -> (X-snd : x2) -> (X-z1261 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P Hterm
Prod-inv-rect-Type1 = λ (l37 l36 l29 : Level) -> λ (x1 : Set l37) -> λ (x2 : Set l36) -> λ (Hterm : Prod l37 l36 x1 x2) -> λ (P : (X-z1260 : Prod l37 l36 x1 x2) -> Set l29) -> λ (H1 : (X-fst : x1) -> (X-snd : x2) -> (X-z1261 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> Prod-rect-Type1 l37 l36 ((l37 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-700 : Prod l37 l36 x1 x2) -> (X-z1261 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm X-x-700) -> P X-x-700) H1 Hterm (refl (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm)

Prod-inv-rect-Type0 : (l37 l36 l29 : Level) -> (x1 : Set l37) -> (x2 : Set l36) -> (Hterm : Prod l37 l36 x1 x2) -> (P : (X-z1266 : Prod l37 l36 x1 x2) -> Set l29) -> (X-H1 : (X-fst : x1) -> (X-snd : x2) -> (X-z1267 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P Hterm
Prod-inv-rect-Type0 = λ (l37 l36 l29 : Level) -> λ (x1 : Set l37) -> λ (x2 : Set l36) -> λ (Hterm : Prod l37 l36 x1 x2) -> λ (P : (X-z1266 : Prod l37 l36 x1 x2) -> Set l29) -> λ (H1 : (X-fst : x1) -> (X-snd : x2) -> (X-z1267 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> P (mk-Prod l37 l36 x1 x2 X-fst X-snd)) -> Prod-rect-Type0 l37 l36 ((l37 ⊔ l36) ⊔ l29) x1 x2 (λ (X-x-702 : Prod l37 l36 x1 x2) -> (X-z1267 : eq (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm X-x-702) -> P X-x-702) H1 Hterm (refl (l37 ⊔ l36) (Prod l37 l36 x1 x2) Hterm)

Prod-discr : (l171 l170 l216 : Level) -> (a1 : Set l171) -> (a2 : Set l170) -> (x : Prod l171 l170 a1 a2) -> (y : Prod l171 l170 a1 a2) -> (X-e : eq (l171 ⊔ l170) (Prod l171 l170 a1 a2) x y) -> match-Prod l171 l170 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc l170) ⊔ (lsuc l171)) ⊔ (lsuc (lsuc l216)))) (λ (X-- : Prod l171 l170 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l216) ⊔ l171) ⊔ l170))) (λ (t0 : a1) -> λ (t1 : a2) -> match-Prod l171 l170 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l216)) ⊔ (lsuc l171)) ⊔ (lsuc l170))) (λ (X-- : Prod l171 l170 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l216) ⊔ l171) ⊔ l170))) (λ (u0 : a1) -> λ (u1 : a2) -> (P : Set l216) -> (X-z45 : (e0 : eq l171 a1 (R0 l171 a1 t0) u0) -> (X-e1 : eq l170 a2 (R1 l171 l170 a1 t0 (λ (x0 : a1) -> λ (p0 : eq l171 a1 t0 x0) -> a2) t1 u0 e0) u1) -> P) -> P) y) x
Prod-discr = λ (l171 l170 l216 : Level) -> λ (a1 : Set l171) -> λ (a2 : Set l170) -> λ (x : Prod l171 l170 a1 a2) -> λ (y : Prod l171 l170 a1 a2) -> λ (Deq : eq (l171 ⊔ l170) (Prod l171 l170 a1 a2) x y) -> eq-rect-Type2 (l171 ⊔ l170) ((lsuc lzero) ⊔ (((lsuc l216) ⊔ l171) ⊔ l170)) (Prod l171 l170 a1 a2) x (λ (x-13 : Prod l171 l170 a1 a2) -> λ (X-x-14 : eq (l171 ⊔ l170) (Prod l171 l170 a1 a2) x x-13) -> match-Prod l171 l170 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l216)) ⊔ (lsuc l171)) ⊔ (lsuc l170))) (λ (X-- : Prod l171 l170 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l216) ⊔ l171) ⊔ l170))) (λ (t0 : a1) -> λ (t1 : a2) -> match-Prod l171 l170 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l216)) ⊔ (lsuc l171)) ⊔ (lsuc l170))) (λ (X-- : Prod l171 l170 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l216) ⊔ l171) ⊔ l170))) (λ (u0 : a1) -> λ (u1 : a2) -> (P : Set l216) -> (X-z45 : (e0 : eq l171 a1 (R0 l171 a1 t0) u0) -> (X-e1 : eq l170 a2 (R1 l171 l170 a1 t0 (λ (x0 : a1) -> λ (p0 : eq l171 a1 t0 x0) -> a2) t1 u0 e0) u1) -> P) -> P) x-13) x) (match-Prod l171 l170 a1 a2 ((lsuc lzero) ⊔ ((l170 ⊔ l171) ⊔ (lsuc l216))) (λ (X-- : Prod l171 l170 a1 a2) -> match-Prod l171 l170 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l216)) ⊔ (lsuc l171)) ⊔ (lsuc l170))) (λ (X-0 : Prod l171 l170 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l216) ⊔ l171) ⊔ l170))) (λ (t0 : a1) -> λ (t1 : a2) -> match-Prod l171 l170 a1 a2 ((lsuc (lsuc lzero)) ⊔ (((lsuc (lsuc l216)) ⊔ (lsuc l171)) ⊔ (lsuc l170))) (λ (X-0 : Prod l171 l170 a1 a2) -> Set ((lsuc lzero) ⊔ (((lsuc l216) ⊔ l171) ⊔ l170))) (λ (u0 : a1) -> λ (u1 : a2) -> (P : Set l216) -> (X-z45 : (e0 : eq l171 a1 (R0 l171 a1 t0) u0) -> (X-e1 : eq l170 a2 (R1 l171 l170 a1 t0 (λ (x0 : a1) -> λ (p0 : eq l171 a1 t0 x0) -> a2) t1 u0 e0) u1) -> P) -> P) X--) X--) (λ (a0 : a1) -> λ (a10 : a2) -> λ (P : Set l216) -> λ (DH : (e0 : eq l171 a1 (R0 l171 a1 a0) a0) -> (X-e1 : eq l170 a2 (R1 l171 l170 a1 a0 (λ (x0 : a1) -> λ (p0 : eq l171 a1 a0 x0) -> a2) a10 a0 e0) a10) -> P) -> DH (refl l171 a1 (R0 l171 a1 a0)) (refl l170 a2 (R1 l171 l170 a1 a0 (λ (x0 : a1) -> λ (p0 : eq l171 a1 a0 x0) -> a2) a10 a0 (refl l171 a1 (R0 l171 a1 a0))))) x) y Deq

eq-pair-fst-snd : (l26 l25 : Level) -> (A : Set l26) -> (B : Set l25) -> (p : Prod l26 l25 A B) -> eq (l26 ⊔ l25) (Prod l26 l25 A B) p (mk-Prod l26 l25 A B (fst l26 l25 A B p) (snd l26 l25 A B p))
eq-pair-fst-snd = λ (l26 l25 : Level) -> λ (A : Set l26) -> λ (B : Set l25) -> λ (p : Prod l26 l25 A B) -> match-Prod l26 l25 A B (l26 ⊔ l25) (λ (X-- : Prod l26 l25 A B) -> eq (l26 ⊔ l25) (Prod l26 l25 A B) X-- (mk-Prod l26 l25 A B (fst l26 l25 A B X--) (snd l26 l25 A B X--))) (λ (X-fst : A) -> λ (X-snd : B) -> refl (l26 ⊔ l25) (Prod l26 l25 A B) (mk-Prod l26 l25 A B X-fst X-snd)) p

fst-eq : (l4 l5 : Level) -> (A : Set l4) -> (B : Set l5) -> (a : A) -> (b : B) -> eq l4 A (fst l4 l5 A B (mk-Prod l4 l5 A B a b)) a
fst-eq = λ (l4 l5 : Level) -> λ (A : Set l4) -> λ (B : Set l5) -> λ (a : A) -> λ (X-b : B) -> refl l4 A a

snd-eq : (l8 l3 : Level) -> (A : Set l8) -> (B : Set l3) -> (a : A) -> (b : B) -> eq l3 B (snd l8 l3 A B (mk-Prod l8 l3 A B a b)) b
snd-eq = λ (l8 l3 : Level) -> λ (A : Set l8) -> λ (B : Set l3) -> λ (X-a : A) -> λ (b : B) -> refl l3 B b

contract-pair : (l52 l51 : Level) -> (A : Set l52) -> (B : Set l51) -> (e : Prod l52 l51 A B) -> eq (l52 ⊔ l51) (Prod l52 l51 A B) (match-Prod l52 l51 A B (l52 ⊔ l51) (λ (X-- : Prod l52 l51 A B) -> Prod l52 l51 A B) (λ (a : A) -> λ (b : B) -> mk-Prod l52 l51 A B a b) e) e
contract-pair = λ (l52 l51 : Level) -> λ (A : Set l52) -> λ (B : Set l51) -> λ (X-clearme : Prod l52 l51 A B) -> match-Prod l52 l51 A B (l52 ⊔ l51) (λ (X-- : Prod l52 l51 A B) -> eq (l52 ⊔ l51) (Prod l52 l51 A B) (match-Prod l52 l51 A B (l52 ⊔ l51) (λ (X-0 : Prod l52 l51 A B) -> Prod l52 l51 A B) (λ (a : A) -> λ (b : B) -> mk-Prod l52 l51 A B a b) X--) X--) (λ (X-fst : A) -> λ (X-snd : B) -> refl (l52 ⊔ l51) (Prod l52 l51 A B) (match-Prod l52 l51 A B (l52 ⊔ l51) (λ (X-- : Prod l52 l51 A B) -> Prod l52 l51 A B) (λ (a : A) -> λ (b : B) -> mk-Prod l52 l51 A B a b) (mk-Prod l52 l51 A B X-fst X-snd))) X-clearme

extract-pair : (l182 l181 l153 l152 : Level) -> (A : Set l182) -> (B : Set l181) -> (C : Set l153) -> (D : Set l152) -> (u : Prod l182 l181 A B) -> (Q : (X-- : A) -> (X--1 : B) -> Prod l153 l152 C D) -> (x : C) -> (y : D) -> (X-- : eq (l153 ⊔ l152) (Prod l153 l152 C D) (match-Prod l182 l181 A B (l153 ⊔ l152) (λ (X-- : Prod l182 l181 A B) -> Prod l153 l152 C D) (λ (a : A) -> λ (b : B) -> Q a b) u) (mk-Prod l153 l152 C D x y)) -> ex l182 (((l153 ⊔ l181) ⊔ l182) ⊔ l152) A (λ (a : A) -> ex l181 (((l153 ⊔ l182) ⊔ l152) ⊔ l181) B (λ (b : B) -> And (l182 ⊔ l181) (l153 ⊔ l152) (eq (l182 ⊔ l181) (Prod l182 l181 A B) (mk-Prod l182 l181 A B a b) u) (eq (l153 ⊔ l152) (Prod l153 l152 C D) (Q a b) (mk-Prod l153 l152 C D x y))))
extract-pair = λ (l182 l181 l153 l152 : Level) -> λ (A : Set l182) -> λ (B : Set l181) -> λ (C : Set l153) -> λ (D : Set l152) -> λ (X-clearme : Prod l182 l181 A B) -> match-Prod l182 l181 A B (((l153 ⊔ l182) ⊔ l152) ⊔ l181) (λ (X-- : Prod l182 l181 A B) -> (Q : (X--1 : A) -> (X--2 : B) -> Prod l153 l152 C D) -> (x : C) -> (y : D) -> (X--1 : eq (l153 ⊔ l152) (Prod l153 l152 C D) (match-Prod l182 l181 A B (l153 ⊔ l152) (λ (X-0 : Prod l182 l181 A B) -> Prod l153 l152 C D) (λ (a : A) -> λ (b : B) -> Q a b) X--) (mk-Prod l153 l152 C D x y)) -> ex l182 (((l153 ⊔ l182) ⊔ l152) ⊔ l181) A (λ (a : A) -> ex l181 (((l153 ⊔ l182) ⊔ l152) ⊔ l181) B (λ (b : B) -> And (l182 ⊔ l181) (l153 ⊔ l152) (eq (l182 ⊔ l181) (Prod l182 l181 A B) (mk-Prod l182 l181 A B a b) X--) (eq (l153 ⊔ l152) (Prod l153 l152 C D) (Q a b) (mk-Prod l153 l152 C D x y))))) (λ (a : A) -> λ (b : B) -> λ (Q : (X-- : A) -> (X--1 : B) -> Prod l153 l152 C D) -> λ (x : C) -> λ (y : D) -> λ (E1 : eq (l153 ⊔ l152) (Prod l153 l152 C D) (Q a b) (mk-Prod l153 l152 C D x y)) -> ex-intro l182 (((l153 ⊔ l182) ⊔ l152) ⊔ l181) A (λ (a0 : A) -> ex l181 (((l153 ⊔ l182) ⊔ l152) ⊔ l181) B (λ (b0 : B) -> And (l182 ⊔ l181) (l153 ⊔ l152) (eq (l182 ⊔ l181) (Prod l182 l181 A B) (mk-Prod l182 l181 A B a0 b0) (mk-Prod l182 l181 A B a b)) (eq (l153 ⊔ l152) (Prod l153 l152 C D) (Q a0 b0) (mk-Prod l153 l152 C D x y)))) a (ex-intro l181 (((l153 ⊔ l181) ⊔ l182) ⊔ l152) B (λ (b0 : B) -> And (l182 ⊔ l181) (l153 ⊔ l152) (eq (l182 ⊔ l181) (Prod l182 l181 A B) (mk-Prod l182 l181 A B a b0) (mk-Prod l182 l181 A B a b)) (eq (l153 ⊔ l152) (Prod l153 l152 C D) (Q a b0) (mk-Prod l153 l152 C D x y))) b (conj (l182 ⊔ l181) (l153 ⊔ l152) (eq (l182 ⊔ l181) (Prod l182 l181 A B) (mk-Prod l182 l181 A B a b) (mk-Prod l182 l181 A B a b)) (eq (l153 ⊔ l152) (Prod l153 l152 C D) (Q a b) (mk-Prod l153 l152 C D x y)) (refl (l182 ⊔ l181) (Prod l182 l181 A B) (mk-Prod l182 l181 A B a b)) E1))) X-clearme

breakup-pair : (l61 l60 l55 l37 : Level) -> (A : Set l61) -> (B : Set l60) -> (C : Set l55) -> (x : Prod l61 l60 A B) -> (R : (X-- : C) -> Set l37) -> (P : (X-- : A) -> (X--1 : B) -> C) -> (X-- : R (P (fst l61 l60 A B x) (snd l61 l60 A B x))) -> R (match-Prod l61 l60 A B l55 (λ (X-0 : Prod l61 l60 A B) -> C) (λ (a : A) -> λ (b : B) -> P a b) x)
breakup-pair = λ (l61 l60 l55 l37 : Level) -> λ (A : Set l61) -> λ (B : Set l60) -> λ (C : Set l55) -> λ (X-clearme : Prod l61 l60 A B) -> match-Prod l61 l60 A B ((lsuc lzero) ⊔ (((l55 ⊔ l61) ⊔ (lsuc l37)) ⊔ l60)) (λ (X-- : Prod l61 l60 A B) -> (R : (X--1 : C) -> Set l37) -> (P : (X--1 : A) -> (X--2 : B) -> C) -> (X--1 : R (P (fst l61 l60 A B X--) (snd l61 l60 A B X--))) -> R (match-Prod l61 l60 A B l55 (λ (X-0 : Prod l61 l60 A B) -> C) (λ (a : A) -> λ (b : B) -> P a b) X--)) (λ (X-fst : A) -> λ (X-snd : B) -> λ (R : (X-- : C) -> Set l37) -> λ (P : (X-- : A) -> (X--1 : B) -> C) -> λ (auto : R (P X-fst X-snd)) -> auto) X-clearme

pair-elim : (l103 l102 l97 l56 : Level) -> (A : Set l103) -> (B : Set l102) -> (C : Set l97) -> (T : (X-- : A) -> (X--1 : B) -> C) -> (p : Prod l103 l102 A B) -> (P : (X-- : Prod l103 l102 A B) -> (X--1 : C) -> Set l56) -> (X-- : (lft : A) -> (rgt : B) -> (X-- : eq (l103 ⊔ l102) (Prod l103 l102 A B) p (mk-Prod l103 l102 A B lft rgt)) -> P (mk-Prod l103 l102 A B lft rgt) (T lft rgt)) -> P p (match-Prod l103 l102 A B l97 (λ (X-0 : Prod l103 l102 A B) -> C) (λ (lft : A) -> λ (rgt : B) -> T lft rgt) p)
pair-elim = λ (l103 l102 l97 l56 : Level) -> λ (A : Set l103) -> λ (B : Set l102) -> λ (C : Set l97) -> λ (T : (X-- : A) -> (X--1 : B) -> C) -> λ (X-clearme : Prod l103 l102 A B) -> match-Prod l103 l102 A B ((lsuc lzero) ⊔ (((l103 ⊔ l97) ⊔ l102) ⊔ (lsuc l56))) (λ (X-- : Prod l103 l102 A B) -> (P : (X--1 : Prod l103 l102 A B) -> (X--2 : C) -> Set l56) -> (X--1 : (lft : A) -> (rgt : B) -> (X--1 : eq (l103 ⊔ l102) (Prod l103 l102 A B) X-- (mk-Prod l103 l102 A B lft rgt)) -> P (mk-Prod l103 l102 A B lft rgt) (T lft rgt)) -> P X-- (match-Prod l103 l102 A B l97 (λ (X-0 : Prod l103 l102 A B) -> C) (λ (lft : A) -> λ (rgt : B) -> T lft rgt) X--)) (λ (X-fst : A) -> λ (X-snd : B) -> λ (P : (X-- : Prod l103 l102 A B) -> (X--1 : C) -> Set l56) -> λ (auto : (lft : A) -> (rgt : B) -> (X-- : eq (l103 ⊔ l102) (Prod l103 l102 A B) (mk-Prod l103 l102 A B X-fst X-snd) (mk-Prod l103 l102 A B lft rgt)) -> P (mk-Prod l103 l102 A B lft rgt) (T lft rgt)) -> auto X-fst X-snd (refl (l103 ⊔ l102) (Prod l103 l102 A B) (mk-Prod l103 l102 A B X-fst X-snd))) X-clearme

pair-elim2 : (l120 l119 l114 l113 l67 : Level) -> (A : Set l120) -> (B : Set l119) -> (C : Set l114) -> (C' : Set l113) -> (T : (X-- : A) -> (X--1 : B) -> C) -> (T' : (X-- : A) -> (X--1 : B) -> C') -> (p : Prod l120 l119 A B) -> (P : (X-- : Prod l120 l119 A B) -> (X--1 : C) -> (X--2 : C') -> Set l67) -> (X-- : (lft : A) -> (rgt : B) -> (X-- : eq (l120 ⊔ l119) (Prod l120 l119 A B) p (mk-Prod l120 l119 A B lft rgt)) -> P (mk-Prod l120 l119 A B lft rgt) (T lft rgt) (T' lft rgt)) -> P p (match-Prod l120 l119 A B l114 (λ (X-0 : Prod l120 l119 A B) -> C) (λ (lft : A) -> λ (rgt : B) -> T lft rgt) p) (match-Prod l120 l119 A B l113 (λ (X-0 : Prod l120 l119 A B) -> C') (λ (lft : A) -> λ (rgt : B) -> T' lft rgt) p)
pair-elim2 = λ (l120 l119 l114 l113 l67 : Level) -> λ (A : Set l120) -> λ (B : Set l119) -> λ (C : Set l114) -> λ (C' : Set l113) -> λ (T : (X-- : A) -> (X--1 : B) -> C) -> λ (T' : (X-- : A) -> (X--1 : B) -> C') -> λ (X-clearme : Prod l120 l119 A B) -> match-Prod l120 l119 A B ((lsuc lzero) ⊔ ((((l119 ⊔ l114) ⊔ l113) ⊔ l120) ⊔ (lsuc l67))) (λ (X-- : Prod l120 l119 A B) -> (P : (X--1 : Prod l120 l119 A B) -> (X--2 : C) -> (X--3 : C') -> Set l67) -> (X--1 : (lft : A) -> (rgt : B) -> (X--1 : eq (l120 ⊔ l119) (Prod l120 l119 A B) X-- (mk-Prod l120 l119 A B lft rgt)) -> P (mk-Prod l120 l119 A B lft rgt) (T lft rgt) (T' lft rgt)) -> P X-- (match-Prod l120 l119 A B l114 (λ (X-0 : Prod l120 l119 A B) -> C) (λ (lft : A) -> λ (rgt : B) -> T lft rgt) X--) (match-Prod l120 l119 A B l113 (λ (X-0 : Prod l120 l119 A B) -> C') (λ (lft : A) -> λ (rgt : B) -> T' lft rgt) X--)) (λ (X-fst : A) -> λ (X-snd : B) -> λ (P : (X-- : Prod l120 l119 A B) -> (X--1 : C) -> (X--2 : C') -> Set l67) -> λ (auto : (lft : A) -> (rgt : B) -> (X-- : eq (l120 ⊔ l119) (Prod l120 l119 A B) (mk-Prod l120 l119 A B X-fst X-snd) (mk-Prod l120 l119 A B lft rgt)) -> P (mk-Prod l120 l119 A B lft rgt) (T lft rgt) (T' lft rgt)) -> auto X-fst X-snd (refl (l120 ⊔ l119) (Prod l120 l119 A B) (mk-Prod l120 l119 A B X-fst X-snd))) X-clearme

pair-eq1 : (l125 l124 : Level) -> (A : Set l125) -> (B : Set l124) -> (a1 : A) -> (a2 : A) -> (b1 : B) -> (b2 : B) -> (X-- : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B a1 b1) (mk-Prod l125 l124 A B a2 b2)) -> eq l125 A a1 a2
pair-eq1 = λ (l125 l124 : Level) -> λ (A : Set l125) -> λ (B : Set l124) -> λ (a1 : A) -> λ (a2 : A) -> λ (b1 : B) -> λ (b2 : B) -> λ (H : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B a1 b1) (mk-Prod l125 l124 A B a2 b2)) -> Prod-discr l125 l124 l125 A B (mk-Prod l125 l124 A B a1 b1) (mk-Prod l125 l124 A B a2 b2) H (eq l125 A a1 a2) (λ (e0 : eq l125 A (R0 l125 A a1) a2) -> eq-ind-r l125 (l125 ⊔ l124) A a2 (λ (x : A) -> λ (X-- : eq l125 A x a2) -> (X--1 : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B x b1) (mk-Prod l125 l124 A B a2 b2)) -> (X-e1 : eq l124 B (R1 l125 l124 A x (λ (x0 : A) -> λ (p0 : eq l125 A x x0) -> B) b1 a2 X--) b2) -> eq l125 A x a2) (λ (H0 : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B a2 b1) (mk-Prod l125 l124 A B a2 b2)) -> λ (e00 : eq l124 B (R1 l125 l124 A a2 (λ (x0 : A) -> λ (p0 : eq l125 A a2 x0) -> B) b1 a2 (refl l125 A a2)) b2) -> eq-ind-r l124 (l125 ⊔ l124) B b2 (λ (x : B) -> λ (X-- : eq l124 B x b2) -> (X--1 : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B a2 x) (mk-Prod l125 l124 A B a2 b2)) -> eq l125 A a2 a2) (λ (H1 : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B a2 b2) (mk-Prod l125 l124 A B a2 b2)) -> streicherK (l125 ⊔ l124) l125 (Prod l125 l124 A B) (mk-Prod l125 l124 A B a2 b2) (λ (X-- : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B a2 b2) (mk-Prod l125 l124 A B a2 b2)) -> eq l125 A a2 a2) (refl l125 A a2) H1) b1 e00 H0) a1 e0 H)

pair-eq2 : (l125 l124 : Level) -> (A : Set l125) -> (B : Set l124) -> (a1 : A) -> (a2 : A) -> (b1 : B) -> (b2 : B) -> (X-- : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B a1 b1) (mk-Prod l125 l124 A B a2 b2)) -> eq l124 B b1 b2
pair-eq2 = λ (l125 l124 : Level) -> λ (A : Set l125) -> λ (B : Set l124) -> λ (a1 : A) -> λ (a2 : A) -> λ (b1 : B) -> λ (b2 : B) -> λ (H : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B a1 b1) (mk-Prod l125 l124 A B a2 b2)) -> Prod-discr l125 l124 l124 A B (mk-Prod l125 l124 A B a1 b1) (mk-Prod l125 l124 A B a2 b2) H (eq l124 B b1 b2) (λ (e0 : eq l125 A (R0 l125 A a1) a2) -> eq-ind-r l125 (l125 ⊔ l124) A a2 (λ (x : A) -> λ (X-- : eq l125 A x a2) -> (X--1 : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B x b1) (mk-Prod l125 l124 A B a2 b2)) -> (X-e1 : eq l124 B (R1 l125 l124 A x (λ (x0 : A) -> λ (p0 : eq l125 A x x0) -> B) b1 a2 X--) b2) -> eq l124 B b1 b2) (λ (H0 : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B a2 b1) (mk-Prod l125 l124 A B a2 b2)) -> λ (e00 : eq l124 B (R1 l125 l124 A a2 (λ (x0 : A) -> λ (p0 : eq l125 A a2 x0) -> B) b1 a2 (refl l125 A a2)) b2) -> eq-ind-r l124 (l125 ⊔ l124) B b2 (λ (x : B) -> λ (X-- : eq l124 B x b2) -> (X--1 : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B a2 x) (mk-Prod l125 l124 A B a2 b2)) -> eq l124 B x b2) (λ (H1 : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B a2 b2) (mk-Prod l125 l124 A B a2 b2)) -> streicherK (l125 ⊔ l124) l124 (Prod l125 l124 A B) (mk-Prod l125 l124 A B a2 b2) (λ (X-- : eq (l125 ⊔ l124) (Prod l125 l124 A B) (mk-Prod l125 l124 A B a2 b2) (mk-Prod l125 l124 A B a2 b2)) -> eq l124 B b2 b2) (refl l124 B b2) H1) b1 e00 H0) a1 e0 H)

pair-destruct-1 : (l69 l68 : Level) -> (A : Set l69) -> (B : Set l68) -> (a : A) -> (b : B) -> (c : Prod l69 l68 A B) -> (X-- : eq (l69 ⊔ l68) (Prod l69 l68 A B) (mk-Prod l69 l68 A B a b) c) -> eq l69 A a (fst l69 l68 A B c)
pair-destruct-1 = λ (l69 l68 : Level) -> λ (A : Set l69) -> λ (B : Set l68) -> λ (a : A) -> λ (b : B) -> λ (X-clearme : Prod l69 l68 A B) -> match-Prod l69 l68 A B (l69 ⊔ l68) (λ (X-- : Prod l69 l68 A B) -> (X--1 : eq (l69 ⊔ l68) (Prod l69 l68 A B) (mk-Prod l69 l68 A B a b) X--) -> eq l69 A a (fst l69 l68 A B X--)) (λ (X-fst : A) -> λ (X-snd : B) -> λ (auto : eq (l69 ⊔ l68) (Prod l69 l68 A B) (mk-Prod l69 l68 A B a b) (mk-Prod l69 l68 A B X-fst X-snd)) -> rewrite-r l69 l69 A X-fst (λ (X-- : A) -> eq l69 A X-- X-fst) (refl l69 A X-fst) a (rewrite-l l69 l69 A (fst l69 l68 A B (mk-Prod l69 l68 A B a b)) (λ (X-- : A) -> eq l69 A X-- X-fst) (rewrite-r (l69 ⊔ l68) l69 (Prod l69 l68 A B) (mk-Prod l69 l68 A B X-fst X-snd) (λ (X-- : Prod l69 l68 A B) -> eq l69 A (fst l69 l68 A B X--) X-fst) (fst-eq l69 l68 A B X-fst X-snd) (mk-Prod l69 l68 A B a b) auto) a (fst-eq l69 l68 A B a b))) X-clearme

pair-destruct-2 : (l69 l68 : Level) -> (A : Set l69) -> (B : Set l68) -> (a : A) -> (b : B) -> (c : Prod l69 l68 A B) -> (X-- : eq (l69 ⊔ l68) (Prod l69 l68 A B) (mk-Prod l69 l68 A B a b) c) -> eq l68 B b (snd l69 l68 A B c)
pair-destruct-2 = λ (l69 l68 : Level) -> λ (A : Set l69) -> λ (B : Set l68) -> λ (a : A) -> λ (b : B) -> λ (X-clearme : Prod l69 l68 A B) -> match-Prod l69 l68 A B (l69 ⊔ l68) (λ (X-- : Prod l69 l68 A B) -> (X--1 : eq (l69 ⊔ l68) (Prod l69 l68 A B) (mk-Prod l69 l68 A B a b) X--) -> eq l68 B b (snd l69 l68 A B X--)) (λ (X-fst : A) -> λ (X-snd : B) -> λ (auto : eq (l69 ⊔ l68) (Prod l69 l68 A B) (mk-Prod l69 l68 A B a b) (mk-Prod l69 l68 A B X-fst X-snd)) -> rewrite-r l68 l68 B X-snd (λ (X-- : B) -> eq l68 B X-- X-snd) (refl l68 B X-snd) b (rewrite-l l68 l68 B (snd l69 l68 A B (mk-Prod l69 l68 A B a b)) (λ (X-- : B) -> eq l68 B X-- X-snd) (rewrite-r (l69 ⊔ l68) l68 (Prod l69 l68 A B) (mk-Prod l69 l68 A B X-fst X-snd) (λ (X-- : Prod l69 l68 A B) -> eq l68 B (snd l69 l68 A B X--) X-snd) (snd-eq l69 l68 A B X-fst X-snd) (mk-Prod l69 l68 A B a b) auto) b (snd-eq l69 l68 A B a b))) X-clearme

coerc-pair-sigma : (l35 l38 l32 : Level) -> (A : Set l35) -> (B : Set l38) -> (P : (X-- : B) -> Set l32) -> (p : Prod l35 l38 A B) -> (X-- : P (snd l35 l38 A B p)) -> Prod l35 (l38 ⊔ l32) A (Sig l38 l32 B (λ (x : B) -> P x))
coerc-pair-sigma = λ (l35 l38 l32 : Level) -> λ (A : Set l35) -> λ (B : Set l38) -> λ (P : (X-- : B) -> Set l32) -> λ (X-clearme : Prod l35 l38 A B) -> match-Prod l35 l38 A B ((l38 ⊔ l35) ⊔ l32) (λ (X-- : Prod l35 l38 A B) -> (X--1 : P (snd l35 l38 A B X--)) -> Prod l35 (l38 ⊔ l32) A (Sig l38 l32 B (λ (x : B) -> P x))) (λ (a : A) -> λ (b : B) -> λ (p : P b) -> mk-Prod l35 (l38 ⊔ l32) A (Sig l38 l32 B (λ (x : B) -> P x)) a (mk-Sig l38 l32 B (λ (x : B) -> P x) b p)) X-clearme

dpi1--o--coerc-pair-sigma : (l26 l29 l21 l19 : Level) -> (x0 : Set l26) -> (x1 : Set l29) -> (x2 : (X-- : Prod l26 l29 x0 x1) -> Set l21) -> (x3 : (X-- : x1) -> Set l19) -> (x4 : DPair (l29 ⊔ l26) l21 (Prod l26 l29 x0 x1) x2) -> (x5 : x3 (snd l26 l29 x0 x1 (dpi1 (l29 ⊔ l26) l21 (Prod l26 l29 x0 x1) x2 x4))) -> Prod l26 (l29 ⊔ l19) x0 (Sig l29 l19 x1 (λ (x : x1) -> x3 x))
dpi1--o--coerc-pair-sigma = λ (l26 l29 l21 l19 : Level) -> λ (x0 : Set l26) -> λ (x1 : Set l29) -> λ (x2 : (X-- : Prod l26 l29 x0 x1) -> Set l21) -> λ (x3 : (X-- : x1) -> Set l19) -> λ (x4 : DPair (l29 ⊔ l26) l21 (Prod l26 l29 x0 x1) x2) -> λ (x5 : x3 (snd l26 l29 x0 x1 (dpi1 (l29 ⊔ l26) l21 (Prod l26 l29 x0 x1) x2 x4))) -> coerc-pair-sigma l26 l29 l19 x0 x1 x3 (dpi1 (l29 ⊔ l26) l21 (Prod l26 l29 x0 x1) x2 x4) x5