Function varisat::unit_simplify::prove_units

pub fn prove_units<'a>(
    ctx: Const<VariablesP, Const<ClauseAllocP, Const<AssignmentP, Mut<TrailP, Mut<SolverStateP, Mut<ProofP<'a>, Mut<ImplGraphP, Ref<Context<'a>>>>>>>>>
) -> bool

Remove satisfied clauses and false literals.