proof.scala

class Nat

case class Add(val l: Nat, val r: Nat) 

extension (a: Add)
  def comm = Add(a.r, a.l)

@main def main =
  val n = Nat()
  val m = Nat()
  val el = Add(n, m)
  val er = Add(m, n)
  println(el.comm == er)