(def-quasi-constructor pair 
  "lambda(a:ind_1,b:ind_2,
        lambda(x:ind_1,y:ind_2, if(a=x and b=y, an%individual, ?unit%sort)))"
  (language pure-generic-theory-2)
  (fixed-theories the-kernel-theory))

(def-quasi-constructor pair? 
  "lambda(p:sets[ind_1,ind_2], forsome(x:ind_1,y:ind_2, p=pair(x,y)))"
  (language pure-generic-theory-2)
  (fixed-theories the-kernel-theory))

(def-quasi-constructor first 
  "lambda(p:sets[ind_1,ind_2], iota(x:ind_1,forsome(y:ind_2, p=pair(x,y))))"
  (language pure-generic-theory-2)
  (fixed-theories the-kernel-theory))

(def-quasi-constructor second 
  "lambda(p:sets[ind_1,ind_2], iota(y:ind_2,forsome(x:ind_1, p=pair(x,y))))"
  (language pure-generic-theory-2)
  (fixed-theories the-kernel-theory))

(def-quasi-constructor i-cross-product 
    "lambda(a:sets[ind_1],b:sets[ind_2],
          indic(p:sets[ind_1,ind_2], pair_q{p} and (first{p} in a) and (second{p} in b)))"
  (language pure-generic-theory-2)
  (fixed-theories the-kernel-theory))

(def-theorem pairs-are-pairs 
    "forall(x:ind_1,y:ind_2, pair_q(pair(x,y)))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        (instantiate-existential ("x" "y"))
        )))

(def-theorem pairs-are-pairs-rewrite 
    "forall(x:ind_1,y:ind_2, pair_q(pair(x,y)) iff truth)"
    (theory pure-generic-theory-2)
    (usages transportable-rewrite)
    (proof
      (
        (apply-macete-with-minor-premises pairs-are-pairs)
        )))

(def-theorem uniqueness-for-pairs 
    "forall(x_1,x_2:ind_1,y_1,y_2:ind_2, 
          pair(x_1,y_1) = pair(x_2,y_2) iff (x_1 = x_2 and y_1 = y_2))" 
    (theory pure-generic-theory-2)
    (usages transportable-macete transportable-rewrite)
    (proof
      (
        direct-inference
        direct-inference
        (block 
            (script-comment "`direct-inference' at (0)")
            (contrapose "with(p:prop,p);")
            extensionality
            (instantiate-existential ("x_1" "y_1"))
            simplify
            (antecedent-inference "with(p:prop,p);")
            simplify
            simplify)
        simplify
        )))

(def-theorem reverse-pairs 
    "forall(x_1,x_2:ind_1,y_1,y_2:ind_2, 
          pair(x_1,y_1) = pair(x_2,y_2) iff pair(y_1,x_1) = pair(y_2,x_2))" 
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        (apply-macete-with-minor-premises tr%uniqueness-for-pairs)
        direct-and-antecedent-inference-strategy
        )))

(def-theorem first-defined-entails-pair 
    "forall(p:sets[ind_1,ind_2], #(first(p)) implies pair_q(p))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (contrapose "with(p:prop, p)")
        (eliminate-iota 0)
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("y%iota"))
        (instantiate-existential ("y"))
        (contrapose "with(p:prop, forall(x:ind_1,y:ind_2,p))")
        (backchain "with(a,b:sets[ind_1,ind_2], a=b)")
        (apply-macete-with-minor-premises pairs-are-pairs)
        )))

(def-theorem second-defined-entails-pair 
    "forall(p:sets[ind_1,ind_2], #(second(p)) implies pair_q(p))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (contrapose "with(p:prop, p)")
        (eliminate-iota 0)
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("y%iota"))
        (instantiate-existential ("x"))
        (contrapose "with(p:prop, forall(x:ind_1,y:ind_2,p))")
        (backchain "with(a,b:sets[ind_1,ind_2], a=b)")
        (apply-macete-with-minor-premises pairs-are-pairs)
        )))

(def-theorem first-projection 
    "forall(x:ind_1,y:ind_2, first(pair(x,y)) = x)"
    (theory pure-generic-theory-2)
    (usages transportable-macete transportable-rewrite simplify-logically-first)
    (proof
      (
        direct-inference
        (eliminate-iota 0)
        (instantiate-existential ("x"))
        (instantiate-existential ("y"))
        (antecedent-inference-strategy (0 1))
        (incorporate-antecedent "with(p:prop, p)")
        (incorporate-antecedent "with(p:prop, p)")
        (apply-macete-with-minor-premises uniqueness-for-pairs)
        simplify
        )))

(def-theorem second-projection 
    "forall(x:ind_1,y:ind_2, second(pair(x,y)) = y)"
    (theory pure-generic-theory-2)
    (usages transportable-macete transportable-rewrite simplify-logically-first)
    (proof; uses first-projection
      (
        direct-inference
        (disable-quasi-constructor second)
        (apply-macete-with-minor-premises reverse-pairs)
        (enable-quasi-constructor second)
        (apply-macete-with-minor-premises tr%first-projection)
        )))

(def-theorem pair-first-second 
    "forall(x:sets[ind_1,ind_2],
          pair_q(x) implies (pair(first(x),second(x)) = x))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (backchain-repeatedly ("with(p:prop, p)"))
        (apply-macete-with-minor-premises first-projection)
        (apply-macete-with-minor-premises second-projection)
        )))

(def-theorem pair-first-second-rewrite 
    "forall(x:sets[ind_1,ind_2],
        (pair(first(x),second(x)) 
        = if(pair_q(x),x,lambda(y:ind_1, z:ind_2, ?unit%sort))))"
    (theory pure-generic-theory-2)
    (usages transportable-rewrite simplify-logically-first)
    (proof
      (
        direct-inference
        (case-split ("pair_q{x}"))
        (apply-macete-with-minor-premises pair-first-second)
        simplify
        extensionality
        direct-inference
        simplify
        direct-inference
        (eliminate-iota 0)
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("y%iota"))
        auto-instantiate-existential
        (contrapose "with(p:prop,not(p))")
        (weaken (0 1 2 4))
        (backchain "with(p:prop,p)")
        (apply-macete-with-minor-premises pairs-are-pairs)
        )))

(def-theorem first-of-a-pair-is-defined 
    "forall(x:sets[ind_1,ind_2], pair_q(x) implies #(first(x)))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (backchain "with(p:prop,p)")
        (apply-macete-with-minor-premises first-projection)
        )))

(def-theorem second-of-a-pair-is-defined 
    "forall(x:sets[ind_1,ind_2], pair_q(x) implies #(second(x)))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (backchain "with(p:prop,p)")
        (apply-macete-with-minor-premises second-projection)
        )))

(def-theorem alternate-uniqueness-for-pairs 
    "forall(x,y:sets[ind_1,ind_2], 
          (pair_q(x) and pair_q(y))
            implies 
          x=y iff (first(x) = first(y) and second(x) = second(y)))"
    (theory pure-generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (weaken (1))
        simplify
        (apply-macete-with-minor-premises first-of-a-pair-is-defined)
        (instantiate-existential ("x_$0" "y_$0"))
        (weaken (1 2))
        simplify
        (apply-macete-with-minor-premises second-of-a-pair-is-defined)
        (incorporate-antecedent "with(y,x:sets[ind_1,ind_2],first{x}=first{y})")
        (incorporate-antecedent "with(y,x:sets[ind_1,ind_2],second{x}=second{y})")
        (backchain-repeatedly 
          ("with(y_$0:ind_2,x_$0:ind_1,x:sets[ind_1,ind_2], x=pair{x_$0,y_$0})"))
        (backchain-repeatedly 
          ("with(y_$2:ind_2,x_$2:ind_1,y:sets[ind_1,ind_2], y=pair{x_$2,y_$2})"))
        (apply-macete-with-minor-premises first-projection)
        (apply-macete-with-minor-premises second-projection)
        (apply-macete-with-minor-premises uniqueness-for-pairs)
        direct-and-antecedent-inference-strategy
        )))

(def-compound-macete rewrite-rules-for-pairs 
    (series
      (repeat
        tr%pairs-are-pairs
        tr%first-projection
        tr%second-projection
        tr%pair-first-second)
      simplify))