[AIGERImporter] Add lowering for justice and fairness properties

Currently the AIGER parser handles bad state and invariant constraints by lowering to both verif.assert and verif.assume respectively, but justice and fairness properties are currently not supported.

Lowering Idea

As per https://fmv.jku.at/papers/BiereHeljankoWieringa-FMV-TR-11-2.pdf we can see that a fairness constraint is semantically something that is described to happen as "infinitely often f" (GF f).
Noted in the LTL dialect docs https://circt.llvm.org/docs/Dialects/LTL/ , always is described conceptually but unfortunately there is no ltl.always operation, only ltl.eventually is implemented thus allowing that G can be represented as $\neg F \neg $:

// global fairness is shared across all justice properties
%ff_f = ltl.eventually %f_lit
%gf_f = ltl.not(ltl.eventually(ltl.not(%ff_f))) 

Moreover a justice property is just a conjunction of fairness constraints:

// local fairness properties for ith justice property
%ff_j = ltl.eventually %j_lit
%gf_j = ltl.not(ltl.eventually(ltl.not(%ff_j))) 

%justice = ltl.and %gf_f %gf_j
verif.assert %justice

I am open and would love to hear any alternative approaches as I feel this lowering idea I have is quite verbose and may cause issues (dependent on backends). I am sure the lowering semantically makes sense according to the spec provided above, but surely there is a cleaner way to express liveness.

Start with the AIGER parser's existing lowering for bad state and invariant constraints, then read the cited LTL dialect documentation and FMV paper. Implement support for justice and fairness properties using the chosen lowering approach, and verify that the resulting assertions preserve the specified liveness semantics.