(claim a+b+c+d
  (Π ([a Nat]
      [b Nat]
      [c Nat]
      [d Nat])
    (= Nat (+ (+ a b) (+ c d)) (+ (+ a c) (+ b d)))))

(claim a+b=c+d
  (Π ([a Nat]
      [b Nat]
      [c Nat]
      [d Nat])
    (→ (= Nat a c) (= Nat b d)
       (= Nat (+ a b) (+ c d)))))