∀ {α : Type} (decls : Array (Std.Sat.AIG.Decl α)) (hinv : Std.Sat.AIG.IsDAG α decls) (acc : String) (idx : ℕ)
  (hidx : idx < decls.size) (lhs rhs : Std.Sat.AIG.Fanin) (elem : decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs),
  lhs.gate < idx ∧ rhs.gate < idx →
    InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun acc idx => PSigma.casesOn idx fun idx hidx => idx)
      ⟨acc ++
          (toString idx ++ toString " -> " ++ toString lhs.gate ++
                        toString (Std.Sat.AIG.toGraphviz.invEdgeStyle lhs.invert) ++
                      toString "; " ++
                    toString idx ++
                  toString " -> " ++
                toString rhs.gate ++
              toString (Std.Sat.AIG.toGraphviz.invEdgeStyle rhs.invert) ++
            toString ";"),
        ⟨lhs.gate, ⋯⟩⟩
      ⟨acc, ⟨idx, hidx⟩⟩