diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp
index 0459e38cde..af2af42452 100644
--- a/src/library/compiler/lcnf.cpp
+++ b/src/library/compiler/lcnf.cpp
@@ -362,7 +362,9 @@ public:
                 minor = args[3];
             else
                 minor = args[4];
-            return visit(mk_app(minor, pr_a, pr_b), root);
+            expr new_e = mk_app(minor, pr_a, pr_b);
+            new_e      = mk_app(new_e, args.size() - 5, args.data() + 5);
+            return visit(new_e, root);
         }
     }
 
diff --git a/tests/lean/run/andCasesOnBug.lean b/tests/lean/run/andCasesOnBug.lean
new file mode 100644
index 0000000000..cd7f6ab7fc
--- /dev/null
+++ b/tests/lean/run/andCasesOnBug.lean
@@ -0,0 +1,28 @@
+inductive FinInt: Nat → Type :=
+  | nil: FinInt 0
+  | next: Bool → FinInt n → FinInt (n+1)
+deriving DecidableEq
+
+def zero (sz: Nat): FinInt sz :=
+  match sz with
+  | 0 => .nil
+  | sz+1 => .next false (zero sz)
+
+inductive Pair :=
+  | mk (sz: Nat) (lhs rhs: FinInt sz)
+
+def makePair?: (n m: (sz: Nat) × FinInt sz) → Option Pair
+  | ⟨sz, lhs⟩, ⟨sz', rhs⟩ =>
+      if EQ: true /\ sz = sz' then
+            have rhs' : FinInt sz := by {
+                cases EQ;
+                case intro left right =>
+                simp [right];
+                exact rhs;
+            };
+            some (Pair.mk sz lhs rhs')
+      else none
+
+def usePair: Pair → Bool := fun ⟨sz, lhs, rhs⟩ => lhs = rhs
+
+#eval (makePair? ⟨8, zero 8⟩ ⟨8, zero 8⟩).map usePair