∀ (aig aig_1 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit),
  aig.decls.size ≤ aig_1.decls.size →
    ∀ (aig_2 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit),
      aig_1.decls.size ≤ aig_2.decls.size → ¬aig.decls.size ≤ aig_2.decls.size → False