Theorem: ProjectivePlane.dual_involution (ProjectivePlane.lean)

State before:
P L : Type
p q r s : P
h : ProjectivePlane P
⊢ let h' := inferInstance;
  h' = h
Tactic:
rfl
State after:
no goals