Type mismatch at application of lemma

Stream: general

[Quinn Culver]

Why isn't have hl₁l₃: l₁ ≠ l₃, from distinct_lines h h₁₃, working below?

import combinatorics.configuration
open configuration.projective_plane

open classical

universe u

variables (P L : Type u) [has_mem P L] [configuration.projective_plane P L]

lemma distinct_lines (p: P) (l₁ l₂ : L)
(h₁: p ∈ l₁) (h₂: p ∉ l₂)  : l₁ ≠ l₂ :=  sorry


lemma axiom_3_alternative: ∃ (a₁ a₂ c₁₃ c₂₃ : P), ∀ (l : L),
  ¬(a₁ ∈ l ∧ a₂ ∈ l ∧ c₁₃ ∈ l)
  ∧ ¬(a₁ ∈ l ∧ a₂ ∈ l ∧ c₂₃ ∈ l)
  ∧ ¬(a₁ ∈ l ∧ c₁₃ ∈ l ∧ c₂₃ ∈ l)
  ∧ ¬(a₂ ∈ l ∧ c₁₃ ∈ l ∧  c₂₃ ∈ l)
  :=
  begin
  have h: ∃(p₁ p₂ p₃ : P) (l₁ l₂ l₃ : L), p₁ ∉ l₂ ∧ p₁ ∉ l₃ ∧
  p₂ ∉ l₁ ∧ p₂ ∈ l₂ ∧ p₂ ∈ l₃ ∧ p₃ ∉ l₁ ∧ p₃ ∈ l₂ ∧ p₃ ∉ l₃,
    from exists_config,
  rcases h with ⟨p₁, p₂, p₃, l₁, l₂, l₃, hr⟩,
  rcases hr with ⟨h₁₂, h₁₃, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩,
  cases classical.em (p₁ ∈ l₁),
  begin
    have hl₁l₃: l₁ ≠ l₃,  from distinct_lines h h₁₃, --Why doesn't this work?

  end,

  begin
    sorry
  end,
  end

The error message is

type mismatch at application
  distinct_lines h
term
  h
has type
  p₁ ∈ l₁ : Prop
but is expected to have type
  Type ? : Type (?+1)

[Sky Wilshaw]

The first parameter of distinct_lines is P. I think you probably want to declare

variables {P L : Type u}

to make the variables implicit.

[Quinn Culver]

Thanks. I also changed lemma distinct_lines (p: P) (l₁ l₂ : L) to lemma distinct_lines {p: P}{l₁ l₂ : L} before the error went away.