∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (h_1 : Unit → motive Std.Sat.AIG.Decl.false)
  (h_2 : (x : Std.Sat.AIG.Decl α) → motive x),
  (match Std.Sat.AIG.Decl.false with
    | Std.Sat.AIG.Decl.false => h_1 ()
    | x => h_2 x) =
    h_1 ()