Require Export Coq.Setoids.Setoid.

(* Very simple first-order logic theorem (illustrating the issue):
  if P is true, then any implication with condition P will be equivalent to the
  consequence *)
Theorem test (P Q : Prop) :
  P -> ((P -> Q) <-> Q).
Proof.
  intros H₁.
  split;
    intros H₂.
    { apply H₂.
      assumption. }
    { intros _.
      assumption. }
Qed.

(* An immediate related result is that any implication with condition the
  "always-true" predicate is equivalent to the consequence.

  This can be proved using setoid rewriting. *)
Theorem test' (P : Prop) :
  (True -> P) <-> P.
Proof.
  setoid_rewrite test.
  { reflexivity. }
  { constructor. }
Qed.

(* The following theorem should also be (in my opinion) provable thanks to
  setoid rewriting (using rewriting under binders), but it fails. *)
Theorem test'_under_binder {T} (PP : T -> Prop) :
  (forall x : T, True -> PP x) <-> forall x : T, PP x.
Proof.
  Fail (setoid_rewrite test).
Abort.

(* However, a slight modification of the lemma type to force a forall being
  used leads to success. *)
Theorem test'_under_binder_working {T} (PP : T -> Prop) :
  (forall x : T, True -> PP x) <-> forall x : T, PP x.
Proof.
  setoid_rewrite (
    @id (forall (P Q : Prop) (H₁ : P), let _ := H₁ in (P -> Q) <-> Q) test
  ).
  { reflexivity. }
  { (* note, importantly, that there is a new x in scope here, so it works as
    expected *)
    constructor. }
Qed.