Proofgold Address

Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition nSubq := λ x0 x1 . not (Subq x0 x1)
Param 4a7ef.. : ι
Param 4ae4a.. : ι → ι
Known efbae.. : ∀ x0 . 4a7ef.. = 4ae4a.. x0 ⟶ ∀ x1 : ο . x1
Theorem c8c18.. : 4a7ef.. = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem 3bafe.. : 4a7ef.. = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Known 4b095.. : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ 4ae4a.. x0 = 4ae4a.. x1 ⟶ ∀ x2 : ο . x2
Theorem 9ac87.. : 4ae4a.. 4a7ef.. = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0 (proof)
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem 1f5f7.. : nIn 4a7ef.. 4a7ef.. (proof)
Theorem 2abd8.. : nIn (4ae4a.. 4a7ef..) 4a7ef.. (proof)
Theorem af2d6.. : nIn (4ae4a.. (4ae4a.. 4a7ef..)) 4a7ef.. (proof)
Known In_irref : ∀ x0 . nIn x0 x0
Theorem 015b8.. : nIn (4ae4a.. 4a7ef..) (4ae4a.. 4a7ef..) (proof)
Theorem ef947.. : nIn (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Known e8942.. : ∀ x0 . Subq 4a7ef.. x0
Theorem 67d30.. : Subq 4a7ef.. 4a7ef.. (proof)
Theorem a90a3.. : Subq 4a7ef.. (4ae4a.. 4a7ef..) (proof)
Theorem f6c3d.. : Subq 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Known f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..)
Theorem 7a6f2.. : nSubq (4ae4a.. 4a7ef..) 4a7ef.. (proof)
Known Subq_ref : ∀ x0 . Subq x0 x0
Theorem 25bc5.. : Subq (4ae4a.. 4a7ef..) (4ae4a.. 4a7ef..) (proof)
Known c79db.. : ∀ x0 . Subq x0 (4ae4a.. x0)
Theorem cfb62.. : Subq (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Known f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 378c0.. : nSubq (4ae4a.. (4ae4a.. 4a7ef..)) 4a7ef.. (proof)
Known 0b783.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 09622.. : nSubq (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. 4a7ef..) (proof)
Theorem 8de7c.. : Subq (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Param ba9d8.. : ι → ο
Known 839f4.. : ∀ x0 : ι → ο . (∀ x1 . ba9d8.. x1 ⟶ (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ba9d8.. x1 ⟶ x0 x1
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known UnionE_impred : ∀ x0 x1 . prim1 x1 (prim3 x0) ⟶ ∀ x2 : ο . (∀ x3 . prim1 x1 x3 ⟶ prim1 x3 x0 ⟶ x2) ⟶ x2
Known 82e3b.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 (4ae4a.. x0) ⟶ Subq x1 x0
Known UnionI : ∀ x0 x1 x2 . prim1 x1 x2 ⟶ prim1 x2 x0 ⟶ prim1 x1 (prim3 x0)
Known 5faa3.. : ∀ x0 . prim1 x0 (4ae4a.. x0)
Theorem 05ab8.. : ∀ x0 . ba9d8.. x0 ⟶ prim3 (4ae4a.. x0) = x0 (proof)
Theorem 72f77.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem c60fe.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 2eaee.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 77d87.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 42824.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 68d02.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 778cc.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 03651.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Theorem ff451.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Theorem a7963.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Theorem 9044c.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Theorem 3b34e.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Theorem 652a2.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Theorem 71fcb.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Theorem 7f899.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Theorem d88ba.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Theorem 15e7b.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Theorem 98e34.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Theorem b9890.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem 102c8.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem 28cca.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem 57aad.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem ea5d5.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem 1ceed.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem 57cc6.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (proof)
Theorem 06ef3.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem 71150.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem 49aa4.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem caeb5.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem d4e8e.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem 69e64.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem 4b5d5.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem cbdee.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (proof)
Theorem 1cd68.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem 4e80f.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem 384d5.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem c8b62.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem 1ebb9.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem 9bb00.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem 0d93c.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem 65954.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Theorem a1e1a.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))))) (proof)
Param In_rec_i : (ι → (ι → ι) → ι) → ι → ι
Param If_i : ο → ι → ι → ι
Definition nat_primrec := λ x0 . λ x1 : ι → ι → ι . In_rec_i (λ x2 . λ x3 : ι → ι . If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm : ∀ x0 : ο . or x0 (not x0)
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Theorem nat_primrec_r : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . ∀ x3 x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ x3 x5 = x4 x5) ⟶ If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0 = If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x4 (prim3 x2))) x0 (proof)
Known In_rec_i_eq : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_i x0 x1 = x0 x1 (In_rec_i x0)
Theorem 1f489.. : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 4a7ef.. = x0 (proof)
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem 239af.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . ba9d8.. x2 ⟶ nat_primrec x0 x1 (4ae4a.. x2) = x1 x2 (nat_primrec x0 x1 x2) (proof)
Definition 616bf.. := λ x0 . nat_primrec x0 (λ x1 . 4ae4a..)
Theorem f30c5.. : ∀ x0 . 616bf.. x0 4a7ef.. = x0 (proof)
Theorem 1c625.. : ∀ x0 x1 . ba9d8.. x1 ⟶ 616bf.. x0 (4ae4a.. x1) = 4ae4a.. (616bf.. x0 x1) (proof)
Known 5c211.. : ∀ x0 : ι → ο . x0 4a7ef.. ⟶ (∀ x1 . ba9d8.. x1 ⟶ x0 x1 ⟶ x0 (4ae4a.. x1)) ⟶ ∀ x1 . ba9d8.. x1 ⟶ x0 x1
Known 2fbbc.. : ∀ x0 . ba9d8.. x0 ⟶ ba9d8.. (4ae4a.. x0)
Theorem 4183e.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ba9d8.. (616bf.. x0 x1) (proof)
Theorem 1319f.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ∀ x2 . ba9d8.. x2 ⟶ 616bf.. (616bf.. x0 x1) x2 = 616bf.. x0 (616bf.. x1 x2) (proof)
Theorem 140e5.. : ∀ x0 . ba9d8.. x0 ⟶ 616bf.. 4a7ef.. x0 = x0 (proof)
Theorem 5cf31.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ 616bf.. (4ae4a.. x0) x1 = 4ae4a.. (616bf.. x0 x1) (proof)
Theorem 1ce6b.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ 616bf.. x0 x1 = 616bf.. x1 x0 (proof)
Definition 14149.. := λ x0 . nat_primrec 4a7ef.. (λ x1 . 616bf.. x0)
Theorem 8940b.. : ∀ x0 . 14149.. x0 4a7ef.. = 4a7ef.. (proof)
Theorem 5ddb9.. : ∀ x0 x1 . ba9d8.. x1 ⟶ 14149.. x0 (4ae4a.. x1) = 616bf.. x0 (14149.. x0 x1) (proof)
Known 4c9b8.. : ba9d8.. 4a7ef..
Theorem 97eb5.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ba9d8.. (14149.. x0 x1) (proof)
Theorem 7ae5f.. : ∀ x0 . ba9d8.. x0 ⟶ 14149.. 4a7ef.. x0 = 4a7ef.. (proof)
Theorem 7639b.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ 14149.. (4ae4a.. x0) x1 = 616bf.. (14149.. x0 x1) x1 (proof)
Theorem 022d0.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ 14149.. x0 x1 = 14149.. x1 x0 (proof)
Theorem a5b99.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ∀ x2 . ba9d8.. x2 ⟶ 14149.. x0 (616bf.. x1 x2) = 616bf.. (14149.. x0 x1) (14149.. x0 x2) (proof)
Theorem 13c0f.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ∀ x2 . ba9d8.. x2 ⟶ 14149.. (616bf.. x0 x1) x2 = 616bf.. (14149.. x0 x2) (14149.. x1 x2) (proof)
Theorem 7ecf1.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . ba9d8.. x1 ⟶ ∀ x2 . ba9d8.. x2 ⟶ 14149.. (14149.. x0 x1) x2 = 14149.. x0 (14149.. x1 x2) (proof)
Theorem 1c51c.. : 616bf.. (4ae4a.. 4a7ef..) (4ae4a.. 4a7ef..) = 4ae4a.. (4ae4a.. 4a7ef..) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0)
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known 3238a.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) (4ae4a.. x0)
Known 054cd.. : ∀ x0 x1 . 4ae4a.. x0 = 4ae4a.. x1 ⟶ x0 = x1
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 893d8.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . prim1 x2 (4ae4a.. x0) ⟶ prim1 (x1 x2) x0) ⟶ not (∀ x2 . prim1 x2 (4ae4a.. x0) ⟶ ∀ x3 . prim1 x3 (4ae4a.. x0) ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) (proof)
Definition bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem aa4b6.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ bij x0 x0 x1 (proof)