1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3886.v b/test-suite/bugs/closed/3886.v
new file mode 100644
index 00000000..2ac4abe5
--- /dev/null
+++ b/test-suite/bugs/closed/3886.v
@@ -0,0 +1,23 @@
+Require Import Program.
+
+Inductive Even : nat -> Prop :=
+| evenO : Even O
+| evenS : forall n, Odd n -> Even (S n)
+with Odd : nat -> Prop :=
+| oddS : forall n, Even n -> Odd (S n).
+
+Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n)
+  := _
+with doubleO {n} (o : Odd n) : Odd (S (2 * n))
+     := _.
+Obligations.
+Axiom cheat : forall {A}, A.
+Obligation 1 of doubleE.
+apply cheat.
+Qed.
+
+Obligation 1 of doubleO.
+apply cheat.
+Qed.
+
+Check doubleE.
+\ No newline at end of file