diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 64b281c788206403ce2d102c5cf489cefb3737fb..ff7858d035f8a98326fa3512c22daf76b3198634 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -85,6 +85,12 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
   | |- @envs_entails ?PROP' _ _ =>
     let x := type_term (eq_refl : @eq Type PROP PROP') in idtac
   | |- let _ := _ in _ => fail
+
+  (* We eta-expand [as_valid_2], in order to make sure that
+     [iStartProof works] even if [PROP] is the carrier type. In this
+     case, typing this expression will end up unifying PROP with
+     [bi_car _], and hence trigger the canonical structures mechanism
+     to find the corresponding bi. *)
   | |- ?φ => eapply (λ P : PROP, @as_valid_2 φ _ P);
                [apply _ || fail "iStartProof: not a Bi entailment"
                |apply tac_adequate]