This module couples the default LRAT implementation to the Formula typeclass.

instance Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.instFormulaPosFinDefaultClause {n : Nat} : Formula (PosFin n) (DefaultClause n) (DefaultFormula n)