Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Claim L0: ∀ x2 : ι → ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ (λ x3 . λ x4 : ι → ι → ι . and (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x5 x6)) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x6 x5))) x0 x2 = (λ x3 . λ x4 : ι → ι → ι . and (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x5 x6)) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x6 x5))) x0 x1
Let x2 of type ι → ι → ι be given.
Assume H0: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4.
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Apply prop_ext_2 with (λ x3 . λ x4 : ι → ι → ι . and (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x5 x6)) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x6 x5))) x0 x2, (λ x3 . λ x4 : ι → ι → ι . and (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x5 x6)) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x6 x5))) x0 x1 leaving 2 subgoals.
Assume H4: (λ x3 . λ x4 : ι → ι → ι . and (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x5 x6)) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x6 x5))) x0 x2.
Apply H4 with (λ x3 . λ x4 : ι → ι → ι . and (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x5 x6)) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x6 x5))) x0 x1.
Assume H5: ∀ x3 . x3 ∈ x0 ⟶ bij x0 x0 (λ x4 . x2 x3 x4).
Assume H6: ∀ x3 . x3 ∈ x0 ⟶ bij x0 x0 (λ x4 . x2 x4 x3).
Apply andI with ∀ x3 . x3 ∈ x0 ⟶ bij x0 x0 (λ x4 . x1 x3 x4), ∀ x3 . ... ⟶ bij x0 x0 (λ x4 . x1 ... ...) leaving 2 subgoals.
...
...
...
Apply unpack_b_o_eq with λ x2 . λ x3 : ι → ι → ι . and (∀ x4 . x4 ∈ x2 ⟶ bij x2 x2 (λ x5 . x3 x4 x5)) (∀ x4 . x4 ∈ x2 ⟶ bij x2 x2 (λ x5 . x3 x5 x4)), x0, x1.
The subproof is completed by applying L0.
■