{α : Type} →
  (motive : Std.Sat.AIG.Decl α → Sort u_1) →
    (x : Std.Sat.AIG.Decl α) →
      (x = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false) →
        ((idx : α) → x = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx)) →
          ((lhs rhs : Std.Sat.AIG.Fanin) → x = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)) →
            motive x