∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (h_1 : Unit → motive Std.Sat.AIG.Decl.false)
  (h_2 : (a : α) → motive (Std.Sat.AIG.Decl.atom a))
  (h_3 : (lhs rhs : Std.Sat.AIG.Fanin) → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match Std.Sat.AIG.Decl.false with
    | Std.Sat.AIG.Decl.false => h_1 ()
    | Std.Sat.AIG.Decl.atom a => h_2 a
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs) =
    h_1 ()