Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∃ x0 x1 x2 : ι → ι → ι → ι → ι → ι . ∃ x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p PtdPred UnaryPredHom struct_id struct_comp x0 x1 x2 x3.
Apply H0 with False.
Let x0 of type ι → ι → ι → ι → ι → ι be given.
Assume H1: (λ x1 : ι → ι → ι → ι → ι → ι . ∃ x2 x3 : ι → ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p PtdPred UnaryPredHom struct_id struct_comp x1 x2 x3 x4) x0.
Apply H1 with False.
Let x1 of type ι → ι → ι → ι → ι → ι be given.
Assume H2: (λ x2 : ι → ι → ι → ι → ι → ι . ∃ x3 : ι → ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p PtdPred UnaryPredHom struct_id struct_comp x0 x2 x3 x4) x1.
Apply H2 with False.
Let x2 of type ι → ι → ι → ι → ι → ι be given.
Assume H3: (λ x3 : ι → ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p PtdPred UnaryPredHom struct_id struct_comp x0 x1 x3 x4) x2.
Apply H3 with False.
Let x3 of type ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H4: MetaCat_pullback_struct_p PtdPred UnaryPredHom struct_id struct_comp x0 x1 x2 x3.
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Apply L9 with False.
Assume H10: and (and (and (and (and (and (and (and (PtdPred (pack_p 1 (λ x4 . True))) (PtdPred (pack_p 1 (λ x4 . True)))) (PtdPred (pack_p 2 (λ x4 . True)))) (UnaryPredHom (pack_p 1 (λ x4 . True)) (pack_p 2 (λ x4 . True)) (lam 1 (λ x4 . 0)))) (UnaryPredHom (pack_p 1 (λ x4 . True)) (pack_p 2 (λ x4 . True)) (lam 1 (λ x4 . 1)))) (PtdPred (x0 (pack_p 1 (λ x4 . True)) (pack_p 1 (λ x4 . True)) (pack_p 2 (λ x4 . True)) (lam 1 (λ x4 . 0)) (lam 1 (λ x4 . 1))))) (UnaryPredHom (x0 (pack_p 1 (λ x4 . True)) (pack_p 1 (λ x4 . True)) (pack_p 2 (λ x4 . True)) (lam 1 (λ x4 . 0)) (lam 1 (λ x4 . 1))) (pack_p 1 (λ x4 . True)) (x1 (pack_p 1 (λ x4 . True)) (pack_p 1 (λ x4 . True)) (pack_p 2 (λ x4 . True)) (lam 1 (λ x4 . 0)) (lam 1 (λ x4 . 1))))) (UnaryPredHom (x0 (pack_p 1 (λ x4 . True)) (pack_p 1 (λ x4 . True)) (pack_p 2 (λ x4 . True)) (lam 1 (λ x4 . 0)) (lam 1 (λ x4 . 1))) (pack_p 1 (λ x4 . True)) (x2 (pack_p 1 (λ x4 . True)) (pack_p 1 (λ x4 . True)) (pack_p 2 (λ x4 . True)) (lam 1 (λ x4 . 0)) (lam 1 (λ x4 . 1))))) (struct_comp (x0 (pack_p 1 (λ x4 . True)) (pack_p 1 (λ x4 . True)) (pack_p 2 (λ x4 . True)) (lam 1 (λ x4 . 0)) ...) ... ... ... ... = ...).
...
■