# Proof witnesses for LAWS.bend. All goals are discharged by normalization.
import Base
import ./LAWS.bend as Laws

def Laws.make_ctor():
  {==}

def Laws.zero_ctor():
  {==}

def Laws.unit_x_ctor():
  {==}

def Laws.unit_y_ctor():
  {==}

def Laws.x_projection():
  {==}

def Laws.y_projection():
  {==}

def Laws.add_zero():
  {==}

def Laws.scale_one():
  {==}

def Laws.sub_self():
  {==}

def Laws.dot():
  {==}

def Laws.length_sq():
  {==}

def Laws.lerp():
  {==}

def Laws.unit_x_dot_unit_y():
  {==}