Some proofs bout pairs

pairs.pie

;; Some proofs about pairs
;; ∀ a b c. a = b → (a, c) = (b, c)
(claim a=b→ac=bc
  (Π ([T U]
      [K U]
      [a T]
      [b T]
      [c K]
      [_ (= T a b)])
    (= (Pair T K) (cons a c) (cons b c))))
(define a=b→ac=bc
  (λ (T K a b c a=b)
    (replace a=b
      (λ (b)
        (= (Pair T K) (cons a c) (cons b c)))
      (same (cons a c)))))

;; ∀ a b c d. a = b & c = d → (a, c) = (b, d)
(claim a=bc=d→ac=bd
  (Π ([T U]
      [K U]
      [a T]
      [b T]
      [c K]
      [d K]
      [_ (= T a b)]
      [_ (= K c d)])
    (= (Pair T K) (cons a c) (cons b d))))
(define a=bc=d→ac=bd
  (λ (T K a b c d a=b c=d)
    (replace c=d
      (λ (d)
        (= (Pair T K) (cons a c) (cons b d)))
      (a=b→ac=bc T K a b c a=b))))

;; ∀ a b c d. (a, c) = (b, d) → a = b & c = d
(claim ac=bd→a=bc=d
  (Π ([T U]
      [K U]
      [a T]
      [b T]
      [c K]
      [d K]
      [_ (= (Pair T K) (cons a c) (cons b d))])
    (Pair (= T a b) (= K c d))))
(define ac=bd→a=bc=d
  (λ (T K a b c d ac=bd)
    (cons
      (replace ac=bd
        (λ (bd)
          (= T a (car bd)))
        (same a))
      (replace ac=bd
        (λ (bd)
          (= K c (cdr bd)))
        (same c)))))