diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean
index d1672a02f6b3..ca2764d91329 100644
--- a/src/Lean/Elab/Coinductive.lean
+++ b/src/Lean/Elab/Coinductive.lean
@@ -50,7 +50,7 @@ structure CoInductiveView : Type where
 
 namespace CoInductiveView
 
-section
+section -- toBinderViews defn
 /--
   Given syntax of the forms
     a) (`:` term)?
diff --git a/tests/lean/run/coindBisim.lean b/tests/lean/run/coindBisim.lean
new file mode 100644
index 000000000000..aa07d751e631
--- /dev/null
+++ b/tests/lean/run/coindBisim.lean
@@ -0,0 +1,87 @@
+structure FSM where
+  S : Type
+  d : S → Nat → S
+  A : S → Prop
+
+-- Example of a coinductive predicate defined over FSMs
+
+coinductive Bisim (fsm : FSM) : fsm.S → fsm.S → Prop :=
+  | step {s t : fsm.S} :
+    (fsm.A s ↔ fsm.A t)
+    → (∀ c, Bisim (fsm.d s c) (fsm.d t c))
+    → Bisim fsm s t
+
+/--
+info: inductive Bisim.Invariant : (fsm : FSM) → (fsm.S → fsm.S → Prop) → fsm.S → fsm.S → Prop
+number of parameters: 4
+constructors:
+Bisim.Invariant.step : ∀ {fsm : FSM} {Bisim : fsm.S → fsm.S → Prop} {x x_1 : fsm.S},
+  (fsm.A x ↔ fsm.A x_1) → (∀ (c : Nat), Bisim (fsm.d x c) (fsm.d x_1 c)) → Bisim.Invariant fsm Bisim x x_1
+-/
+#guard_msgs in
+#print Bisim.Invariant
+
+/--
+info: @[reducible] def Bisim.Is : (fsm : FSM) → (fsm.S → fsm.S → Prop) → Prop :=
+fun fsm R => ∀ {x x_1 : fsm.S}, R x x_1 → Bisim.Invariant fsm R x x_1
+-/
+#guard_msgs in
+#print Bisim.Is
+
+/--
+info: def Bisim : (fsm : FSM) → fsm.S → fsm.S → Prop :=
+fun fsm x x_1 => ∃ R, Bisim.Is fsm R ∧ R x x_1
+-/
+#guard_msgs in
+#print Bisim
+
+/-- info: 'Bisim' does not depend on any axioms -/
+#guard_msgs in
+#print axioms Bisim
+
+theorem bisim_refl : Bisim f a a := by
+  exists fun a b => a = b
+  simp only [and_true]
+  intro s t seqt
+  constructor <;> simp_all
+
+theorem bisim_symm (h : Bisim f a b): Bisim f b a := by
+  rcases h with ⟨rel, relIsBisim, rab⟩
+  exists fun a b => rel b a
+  simp_all
+  intro a b holds
+  specialize relIsBisim holds
+  rcases relIsBisim with ⟨imp, z⟩
+  constructor <;> simp_all only [implies_true, and_self]
+
+theorem Bisim.unfold {f} : Bisim.Is f (Bisim f) := by
+  rintro s t ⟨R, h_is, h_Rst⟩
+  constructor
+  · exact (h_is h_Rst).1
+  · intro c; exact ⟨R, h_is, (h_is h_Rst).2 c⟩
+
+theorem bisim_trans (h_ab : Bisim f a b) (h_bc : Bisim f b c) :
+    Bisim f a c := by
+  exists (fun s t => ∃ u, Bisim f s u ∧ Bisim f u t)
+  constructor
+  intro s t h_Rst
+  · rcases h_Rst with ⟨u, h_su, h_ut⟩
+    have ⟨h_su₁, h_su₂⟩ := h_su.unfold
+    have ⟨h_ut₁, h_ut₂⟩ := h_ut.unfold
+    refine ⟨?_, ?_⟩
+    · rw [h_su₁, h_ut₁]
+    · intro c; exact ⟨_, h_su₂ c, h_ut₂ c⟩
+  · exact ⟨b, h_ab, h_bc⟩
+
+/-- info: 'bisim_refl' depends on axioms: [propext, Quot.sound] -/
+#guard_msgs in
+#print axioms bisim_refl
+
+/-- info: 'bisim_symm' depends on axioms: [propext, Quot.sound] -/
+#guard_msgs in
+#print axioms bisim_symm
+
+/-- info: 'bisim_trans' depends on axioms: [propext] -/
+#guard_msgs in
+#print axioms bisim_trans
+
diff --git a/tests/lean/run/coindTypes.lean b/tests/lean/run/coindTypes.lean
new file mode 100644
index 000000000000..e2b44ffe43b2
--- /dev/null
+++ b/tests/lean/run/coindTypes.lean
@@ -0,0 +1,7 @@
+-- Coinductive currently does only work on Prop
+
+/-- error: Expected return type to be a Prop -/
+#guard_msgs in
+coinductive S (α : Type) : Type :=
+  | cons (hd : α) (tl : S α)
+