Using an axiom with "let"

Stream: new members

[Quinn Culver]

From this lean 3 project, I got the following

constant Point : Type
constant Line : Type
constant lies_on : Point → Line → Prop
constant line_of_points (p₁ p₂ : Point) : p₁ ≠ p₂ → Line

axiom line_exists (p₁ p₂ : Point) (h : p₁ ≠ p₂) :
  let l : Line := line_of_points p₁ p₂ h in
    lies_on p₁ l ∧ lies_on p₂ l

How would one use line_exists in a proof? The fact that it's a let statement is giving me trouble. In particular, suppose the local context contains

p₁p₂: Point
l: Line
h: p₁ ≠ p₂
g_1: lies_on p₁ l
g_2: lies_on p₂ l
l₀: Line := line_of_points p₁ p₂ h

Could line_exists be used to show l = l₀?

[Mario Carneiro]

no, at least not with those axioms alone

[Mario Carneiro]

line_exists could be used to show that lies_on p₁ l₀ and lies_on p₂ l₀ but you need some uniqueness assumption to prove l = l₀

[Quinn Culver]

Thanks. Doesn't uniqueness follow from the fact that line_of_points is a function?

I see.