{α : Type} →
  (decls : Array (Std.Sat.AIG.Decl α)) →
    (motive : Id (String × Std.HashSet (Fin decls.size)) → Sort u_1) →
      (x : Id (String × Std.HashSet (Fin decls.size))) →
        ((dag : String) → (s : Std.HashSet (Fin decls.size)) → motive (dag, s)) → motive x