L_must_be_true.v

Definition Eq {A} (x y : A) := forall (P : A -> Type), P x -> P y.
Definition refl {A} {x : A} : Eq x x := fun P p_x => p_x.
Definition symm {A} {x y : A} (H : Eq x y) : Eq y x :=
  fun P p_y => H (fun z => P z -> P x) (fun x => x) p_y.

Lemma L_must_be_true (
  L_is_false : forall {T} {x y : T} (H : Eq x y),
    Eq H (fun P => symm H (fun z => P z -> P y) (fun x => x)) -> False
  ) : False.
  exact (L_is_false _ I I refl refl).
Qed.