Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιο be given.
Assume H0: ∀ x1 . x0 x1∀ x2 . x0 x2x0 (setprod x1 x2).
Assume H1: ∀ x1 . x0 x1∀ x2 . x0 x2x0 (setexp x2 x1).
Apply andI with MetaCat_product_constr_p x0 HomSet lam_id (λ x1 x2 x3 x4 x5 . lam_comp x1 x4 x5) setprod (λ x1 x2 . lam (setprod x1 x2) (λ x3 . ap x3 0)) (λ x1 x2 . lam (setprod x1 x2) (λ x3 . ap x3 1)) (λ x1 x2 x3 x4 x5 . lam x3 (λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (ap x4 x6) (ap x5 x6)))), ∀ x1 x2 . x0 x1x0 x2MetaCat_exp_p x0 HomSet lam_id (λ x3 x4 x5 x6 x7 . lam_comp x3 x6 x7) setprod (λ x3 x4 . lam (setprod x3 x4) (λ x5 . ap x5 0)) (λ x3 x4 . lam (setprod x3 x4) (λ x5 . ap x5 1)) (λ x3 x4 x5 x6 x7 . lam x5 (λ x8 . lam 2 (λ x9 . If_i (x9 = 0) (ap x6 x8) (ap x7 x8)))) x1 x2 ((λ x3 x4 . setexp x4 x3) x1 x2) ((λ x3 x4 . lam (setprod (setexp x4 x3) x3) (λ x5 . ap (ap x5 0) (ap x5 1))) x1 x2) ((λ x3 x4 x5 x6 . lam x5 (λ x7 . lam x3 (λ x8 . ap x6 (lam 2 (λ x9 . If_i (x9 = 0) x7 x8))))) x1 x2) leaving 2 subgoals.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H2: x0 x1.
Assume H3: x0 x2.
Apply and6I with x0 x1, x0 x2, x0 (setprod x1 x2), HomSet (setprod x1 x2) x1 ((λ x3 x4 . lam (setprod x3 x4) (λ x5 . ap x5 0)) x1 x2), HomSet (setprod x1 x2) x2 ((λ x3 x4 . lam (setprod x3 x4) (λ x5 . ap x5 1)) x1 x2), ∀ x3 . ...∀ x4 x5 . ......and (and (and (HomSet x3 (setprod x1 x2) ((λ x6 x7 x8 x9 x10 . lam x8 (λ x11 . lam 2 (λ x12 . If_i (x12 = 0) (ap x9 x11) (ap x10 x11)))) x1 x2 x3 x4 x5)) (lam x3 (λ x6 . ap ((λ x7 x8 . lam (setprod x7 x8) (λ x9 . ap x9 0)) x1 x2) (ap ... ...)) = ...)) ...) ... leaving 6 subgoals.
...
...
...
...
...
...
...