diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index 4d01b4344260..d0970f821283 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -564,6 +564,19 @@ theorem apply_cond (f : α → β) {b : Bool} {a a' : α} :
     f (bif b then a else a') = bif b then f a else f a' := by
   cases b <;> simp
 
+
+/--
+`dcond b (fun h => x) (fun h => y)` is the same as `if h _ : b then x else y`,
+but optimized for a boolean condition. It can also be written as `bif b then x else y`.
+This is `@[macro_inline]` because `x` and `y` should not be eagerly evaluated (see `dite`).
+This definition intendend for metaprogramming use, and does not come with a suitable API.
+-/
+@[macro_inline]
+protected def dcond {α : Sort u} (c : Bool) (x : c = true → α) (y : c = false → α) : α :=
+  match c with
+  | true  => x rfl
+  | false => y rfl
+
 /-! # decidability -/
 
 protected theorem decide_coe (b : Bool) [Decidable (b = true)] : decide (b = true) = b := decide_eq_true
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 6adab693907f..e3207ccbbb05 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -547,7 +547,16 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
       mkLambdaFVars #[h] f'
     let u ← getLevel goal
     return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
-
+  | cond _α c t f =>
+    let c' ← foldAndCollect oldIH newIH isRecCall c
+    let t' ← withLocalDecl `h .default (← mkEq c' (toExpr true)) fun h => M2.branch do
+      let t' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall t
+      mkLambdaFVars #[h] t'
+    let f' ← withLocalDecl `h .default (← mkEq c' (toExpr false)) fun h => M2.branch do
+      let f' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall f
+      mkLambdaFVars #[h] f'
+    let u ← getLevel goal
+    return mkApp4 (mkConst ``Bool.dcond [u]) goal c' t' f'
   | _ =>
 
   -- we look in to `PProd.mk`, as it occurs in the mutual structural recursion construction
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index c1e2035dfc9e..04ea2ebac663 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -139,13 +139,13 @@ def with_ite_tailrec : Nat → Nat
     if n % 2 = 0 then
       with_ite_tailrec n
     else
-      with_ite_tailrec n
+      with_ite_tailrec (n-1)
 termination_by n => n
 
 /--
 info: with_ite_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ)
-  (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive n.succ) (a✝ : Nat) : motive a✝
+  (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive (n - 1) → motive n.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check with_ite_tailrec.induct
@@ -201,6 +201,24 @@ info: with_dite_tailrec.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), x
 #guard_msgs in
 #check with_dite_tailrec.induct
 
+set_option linter.unusedVariables false in
+def with_bif_tailrec : Nat → Nat
+  | 0 => 0
+  | n+1 =>
+    bif n % 2 == 0 then
+      with_bif_tailrec n
+    else
+      with_bif_tailrec (n-1)
+termination_by n => n
+
+/--
+info: with_bif_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
+  (case2 : ∀ (n : Nat), (n % 2 == 0) = true → motive n → motive n.succ)
+  (case3 : ∀ (n : Nat), (n % 2 == 0) = false → motive (n - 1) → motive n.succ) (a✝ : Nat) : motive a✝
+-/
+#guard_msgs in
+#check with_bif_tailrec.induct
+
 set_option linter.unusedVariables false in
 def with_match_refining_tailrec : Nat → Nat
   | 0 => 0